# Publications

## Work in progress

F. Shmarov,** P. Zuliani**. *Probabilistic Bounded Reachability for Hybrid Systems with Continuous Nondeterministic and Probabilistic Parameters*.

## Journals

O. Oyebamiji, D. Wilkinson, P. G. Jayathilake, S. Rushton, B. Bridgens, B. Li, **P. Zuliani**. *A Bayesian approach to modelling the impact of hydrodynamic shear stress on biofilm deformation. *PLoS One, to appear.

P. G. Jayathilake, P. Gupta, B. Li, C. Madsen, O. Oyebamiji, R. González-Cabaleiro, S. Rushton, B. Bridgens, D. Swailes, B. Allen, S. McGough, **P. Zuliani**, I. D. Ofiteru, D. Wilkinson, J. Chen, T. Curtis. *A Mechanistic Individual-based Model of Microbial Communities*. PLoS One, 12(8): e0181965, 2017.

G. Misirli, M. Cavaliere, W. Waites, M. Pocock, C. Madsen, O. Gilfellon, R. Honorato-Zimmer, **P. Zuliani**, V. Danos, and A. Wipat. *Annotation of rule-based models with formal semantics to enable creation, analysis, reuse and visualisation*. Bioinformatics, 32(6):908-917, 2016.

**P. Zuliani**. *Statistical Model Checking for Biological Applications*. Software Tools for Technology Transfer, 17(4):527-536, 2015.

J. Rusakovica, J. Hallinan, A. Wipat, **P. Zuliani**. *Probabilistic latent semantic analysis applied to whole bacterial genomes identifies common genomic features*. Journal of Integrative Bioinformatics, 11(2):243, 2014.

**P. Zuliani**, A. Platzer, E. M. Clarke. *Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification*. Formal Methods in System Design, 43(2):338-367, 2013.

H. Gong, **P. Zuliani**, E. M. Clarke. *Model checking of a synchronous diabetes-cancer logical network*. Current Bioinformatics, 8(1):9-15, 2013.

H. Gong,** P. Zuliani**, A. Komuravelli, J. R. Faeder, E. M. Clarke. *Analysis and Verification of the HMGB1 Signaling Pathway*. BMC Bioinformatics 2010, 11(Suppl 7):S10. (**Best Paper Award** at InCoB 2010.) **Highly accessed**

**P. Zuliani**. *Reasoning about faulty quantum programs*. Acta Informatica, 46(6):403-432, 2009.

**P. Zuliani**. *Compiling quantum programs*. Acta Informatica, 41(7-8):435–474, 2005.

G. Succi, W. Pedrycz, S. Djokic, **P. Zuliani**, and B. Russo. *An empirical exploration of the distributions of the Chidamber and Kemerer object-oriented metrics suite*. Empirical Software Engineering, 10(1):81–104, 2005.

**P. Zuliani**. *Logical reversibility*. IBM Journal of Research and Development, 45(6):807–818, 2001.

## Tutorial Papers

E. M. Clarke, W. Klieber, M. Nováček, **P. Zuliani**. *Model checking and the state explosion problem.* In 8th LASER Summer School on Software Engineering, Sept. 4-10, 2011. LNCS volume 7682, pp. 1-30, 2012.

## Conferences

J. Revell, **P. Zuliani**. *Stochastic Rate Parameter Inference using the Cross-Entropy Method*. CMSB 2018, to appear.

M. Vasileva, **P. Zuliani**. *An Evaluation of Estimation Techniques for Probabilistic Reachability*. SNR 2018, to appear.

L. Anticoli, C. Piazza, L. Taglialegne, **P. Zuliani**. *Entangλe: A Translation Framework from Quipper Programs to Quantum Markov Chains*. InfQ 2017, to appear.

F. Shmarov, N. Paoletti, E. Bartocci, S. Lin, S.A. Smolka, **P. Zuliani**. *SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems*. In HVC 2017: 13th Haifa Verification Conference. LNCS volume 10629, pp. 131-146, 2017.

F. Shmarov, **P. Zuliani**. *Probabilistic Hybrid Systems Verification via SMT and Monte Carlo Techniques*. In HVC 2016: 12th Haifa Verification Conference. LNCS volume 10028, pp. 152-168, 2016.

N. Miskov-Zivanov, **P. Zuliani**, Q. Wang, E. M. Clarke and J. R. Faeder. *High-level modeling and verification of cellular signaling*. In HLDVT 2016: 18th IEEE International High Level Design Validation and Test Workshop. IEEE, pp. 162-169, 2016.

L. Anticoli, C. Piazza, L. Taglialegne, **P. Zuliani**. *Verifying Quantum Programs: From Quipper Circuits to QPMC*. In RC 2016: 8th Conference on Reversible Computation. LNCS volume 9720, pp. 213-219, 2016.

F. Shmarov, **P. Zuliani**. *SMT-Based Reasoning for Uncertain Hybrid Domains*. In AAAI-16 Workshop on Planning for Hybrid Systems, 30th AAAI Conference on Artificial Intelligence, 2016.

C. Madsen, F. Shmarov, **P. Zuliani**. *BioPSy: An SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models*. Download: [BioPSy]. In CMSB 2015: 13th Conference on Computational Methods in Systems Biology. LNCS volume 9308, pp. 182-194, 2015.

Q. Wang,** P. Zuliani**, S. Kong, S. Gao, E. M. Clarke.* SReach: A Bounded Model Checker for Stochastic Hybrid Systems*. Download: [SReach]. In CMSB 2015: 13th Conference on Computational Methods in Systems Biology. LNCS volume 9308, pp. 15-27, 2015.

F. Shmarov, **P. Zuliani**. *ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems*. Download: [ProbReach]. In HSCC 2015: 18th International Conference on Hybrid Systems: Computation and Control. ACM, pp. 134-139, 2015.

B. Liu, S. Kong, S. Gao,** P. Zuliani**, E. M. Clarke. *Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis*. In HSCC 2015: 18th International Conference on Hybrid Systems: Computation and Control. ACM, pp. 227-232, 2015.

B. Liu, S. Kong, S. Gao,** P. Zuliani**, E. M. Clarke. *Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions*. In CMSB 2014: 12th Conference on Computational Methods in Systems Biology. LNCS volume 8859, pp. 99-113, 2014.

N. Miskov-Zivanov, **P. Zuliani**, E. M. Clarke, J. R. Faeder. *Studies of biological networks with statistical model checking: application to immune system cells*. In ACM-BCB 2013: ACM Conference on Bioinformatics, Computational Biology and Biomedical Informatics. (Poster presentation, *to appear*.)

D. Henriques, J. Martins, **P. Zuliani**, A. Platzer, E. M. Clarke. *Statistical model checking for Markov decision processes*. In QEST 2012: 9th International Conference on Quantitative Evaluation of SysTems. IEEE, pp. 84-93.

**P. Zuliani**, N. Miskov-Zivanov, J. R. Faeder, E. M. Clarke. *Model checking for studying timing of events in T cell differentiation*. In IWBDA 2012: 4th International Workshop on Bio-Design Automation, with 49th ACM/EDAC/IEEE Design Automation Conference (*abstract,* *to appear*).

**P. Zuliani**, C. Baier, E.M. Clarke. *Rare-Event Verification for Stochastic Hybrid Systems*. In HSCC 2012: 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 217-226, 2012.

H. Gong, **P. Zuliani**, Q. Wang, E. M. Clarke. *Formal Analysis for Logical Models of Pancreatic Cancer*. In CDC-ECC 2011: 50th IEEE Conference on Decision and Control and European Control Conference. IEEE, pp. 4855-4860, 2011.

E. M. Clarke and **P. Zuliani**. *Statistical Model Checking for Cyber-Physical Systems*. In ATVA 2011: 9th International Symposium on Automated Technology for Verification and Analysis. LNCS volume 6996, pp. 1-12, 2011. (**Invited paper**.)

H. Gong, **P. Zuliani**, E. M. Clarke. *Model Checking of a Diabetes-Cancer Model*. In CMLS 2011: 3rd International Symposium on Computational Models for Life Sciences, AIP Conf. Proc. 1371, pp. 234-243, 2011.

H. Gong, Q. Wang,** P. Zuliani**, J. R. Faeder, M. T. Lotze, E. M. Clarke. *Symbolic Model Checking of Signaling Pathways in Pancreatic Cancer*. In BiCoB 2011: 3rd International Conference on Bioinformatics and Computational Biology, March 23-25, 2011, New Orleans, LA.

Y.-C. Wang, A. Komuravelli, **P. Zuliani**, E. M. Clarke.* Analog Circuit Verification by Statistical Model Checking*. In ASP-DAC 2011: 16th Asia and South Pacific Design Automation Conference. IEEE, pp. 1-6, 2011. (**Best Paper Award nomination**.)

H. L. S. Younes, E. M. Clarke, **P. Zuliani**. *Statistical Verification of Probabilistic Properties with Unbounded Until*. In SBMF 2010: 13th Brazilian Symposium on Formal Methods. LNCS volume 6527, pp. 144-160, 2011.

H. Gong,** P. Zuliani**, A. Komuravelli, J. R. Faeder, E. M. Clarke. *Computational Modeling and Verification of Signaling Pathways in Cancer*. In ANB 2010: 4th International Conference on Algebraic and Numeric Biology. LNCS volume 6479, pp. 117-135, 2010.

**P. Zuliani**, A. Platzer, E. M. Clarke. *Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification*. In HSCC 2010: 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 243-252, 2010.

S. K. Jha, E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer,** P. Zuliani**. *A Bayesian approach to model checking biological systems*. In CMSB '09: 7th Conference on Computational Methods in Systems Biology. LNCS volume 5688, pp. 218-234, 2009.

**P. Zuliani**. *A formal derivation of Grover’s quantum search algorithm*. In TASE ’07: 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, pp. 67–74, 2007.

**P. Zuliani**. *Quantum programming with mixed states*. In QPL ’05: 3rd International Workshop on Quantum Programming Languages. Electronic Notes in Theoretical Computer Science, volume 170, pp. 185–199, 2007.

**P. Zuliani**. *On counterfactual computation*. In UC ’05: 4th International Conference on Unconventional Computation. LNCS, volume 3699, pp. 251–266, 2005.

**P. Zuliani**. *Non-deterministic quantum programming*. In QPL ’04: 2nd International Workshop on Quantum Programming Languages, pp. 179–195. TUCS Publication 33, Turku, Finland, 2004.

J. W. Sanders and **P. Zuliani**. *Quantum programming*. In MPC ’00: Mathematics of Program Construction. LNCS, volume 1837, pp. 80–99, 2000.

B. Rossi, B. Russo, **P. Zuliani**, and G. Succi. *On the transition to an open source solution for desktop automation*. In TCGOV ’05: ESF-TCD Conference on e-Government. LNCS, volume 3416, pp. 277–285, 2005.

A. Janes, B. Russo, **P. Zuliani**, and G. Succi. *An empirical analysis on the discontinuous use of pair programming*. In XP ’03: 4th International Conference on eXtreme Programming and Agile Processes in Software Engineering. LNCS, volume 2675, pp. 205–214, 2003.* *

* *