**Work in progress**

* *

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

**Journals **

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**

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.

**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

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*).

**, C. Baier, E.M. Clarke.**

P. Zuliani

P. Zuliani

*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.* *