Papers
Preprints
 Quantum Computer Benchmarking via Quantum Algorithms [arXiv]
K. Georgopoulos, C. Emary, P. Zuliani. 2021.
 Investigating the growth of an engineered strain of Cyanobacteria with an AgentBased Model and a Recurrent Neural Network [bioRxiv]
J. Sakkos, J. Weaver, C. Robertson, B. Li, D. Taniguchi, K. Maheshwari, D. Ducat, P. Zuliani, A. S. McGough, T. P Curtis, M. FuentesCabrera. 2021
Tutorials
 Model checking and the state explosion problem [pdf]
E. M. Clarke, W. Klieber, M. Nováček, P. Zuliani
In 8th LASER Summer School on Software Engineering, Sept. 410, 2011. LNCS volume 7682, pp. 130, 2012.
Journals
 Cooperation between autotrophic and heterotrophic denitrifiers under low C/N ratios revealed by individualbased modelling [doi]
W. Xing, D. Gao, Y. Wang, B. Li, Z. Zhang, P. Zuliani, H. Yao, T. P. Curtis
Science of The Total Environment, vol 921, 171091, 2024.
 Formal Verification of Quantum Programs: Theory, Tools and Challenges [arXiv][doi]
M. Lewis, S. Soudjani, P. Zuliani
ACM Transactions on Quantum Computing, to appear, 2023.
 Predicting partner fitness based on spatial structuring in a lightdriven microbial community [doi]
J. K. Sakkos, M. SantosMerino, E. J. Kokarakis, B. Li, M. FuentesCabrera, P. Zuliani, D. C. Ducat
PLOS Computational Biology, to appear, 2023.
 Individualised computational modelling of immune mediated disease onset, flare and clearance in psoriasis [doi]
F. Shmarov, G.R. Smith, S.C. Weatherhead, N.J. Reynolds, P. Zuliani
PLOS Computational Biology, 18(9): e1010267, 2022.
 Coupled CFDDEM modeling to predict how EPS affects bacterial biofilm deformation, recovery and detachment under flow conditions
[doi]
Y. Xia, P. G. Jayathilake, B. Li, P. Zuliani, D. Deehan, J. Longyear, P. Stoodley, J. Chen
Biotechnology and Bioengineering, 119, 25512563, 2022.
 Modelling and Simulating the Noisy Behaviour of Nearterm Quantum Computers [arXiv]
K. Georgopoulos, C. Emary, P. Zuliani
Physical Review A 104, 062432, 2021.
 The use of psoriasis biomarkers, including trajectory of clinical response, to predict clearance and remission duration to UVB phototherapy
[doi]
N. Watson, N. Wilson, F. Shmarov, P. Zuliani, N. J. Reynolds, S. C. Weatherhead
Journal of the European Academy of Dermatology & Venereology 35: 22502258, 2021
 A Comparison of Quantum Walk Implementations on Noisy IntermediateScale Quantum Computers [arXiv]
K. Georgopoulos, C. Emary, P. Zuliani
Physical Review A 103, 022408, 2021.
 CFDDEM modelling of biofilm streamer oscillations and their cohesive failure in fluid flow [doi]
Y. Xia, P. G. Jayathilake, B. Li, P. Zuliani, J. Chen
Biotechnology and Bioengineering 118: 918–929, 2021.
 Automated Synthesis of Safe Digital Controllers for SampledData Stochastic Nonlinear Systems [doi]
F. Shmarov, S. Soudjani, N. Paoletti, E. Bartocci, S. Lin, S. A. Smolka, P. Zuliani
IEEE Access 8:180825180843, 2020.
 Pathways to cellular supremacy in biocomputing [doi]
L. Grozinger, M. Amos, T. Gorochowski, P. Carbonell, D. Oyarzún, R. Stoof, H. Fellermann, P. Zuliani, H. Tas, A. GoniMoreno
Nature Communications 10, 5250 (2019).
 NUFEB: A Massively Parallel Simulator for Individualbased Modelling of Microbial Communities [doi]
B. Li, D. Taniguchi, J. P. Gedara, V. Gogulancea, R. GonzalezCabaleiro, J. Chen, A. S. McGough, I. D. Ofiteru, T. P. Curtis, P. Zuliani
PLOS Computational Biology, 15(12): e1007125, 2019.
 Modelling bacterial twitching in fluid flows: a CFDDEM approach [doi]
P. G. Jayathilake, B. Li, P. Zuliani, T. P. Curtis, J. Chen
Scientific Reports 9, 14540 (2019).
 Individual based model links thermodynamics, chemical speciation and environmental conditions to microbial growth [doi]
V. Gogulancea, R. GonzalezCabaleiro, B. Li, D. Taniguchi, P. G. Jayathilake, J. Chen, D. Wilkinson, D. Swailes, A. S. McGough, P. Zuliani, I. D. Ofiteru, T. P. Curtis
Frontiers Microbiology 10:1871, 2019.
 Bayesian emulation and calibration of an individualbased model of microbial communities [doi]
O. Oyebamiji, D. Wilkinson, B. Li, P. G. Jayathilake, P. Zuliani, T. P. Curtis
Journal of Computational Science 30:194208, 2019.
 A Bayesian approach to modelling the impact of hydrodynamic shear stress on biofilm deformation [doi]
O. Oyebamiji, D. Wilkinson, P. G. Jayathilake, S. Rushton, B. Bridgens, B. Li, P. Zuliani
PLOS ONE 13(4): e0195484, 2018.
 A Mechanistic Individualbased Model of Microbial Communities [doi]
P. G. Jayathilake, P. Gupta, B. Li, C. Madsen, O. Oyebamiji, R. GonzálezCabaleiro, S. Rushton, B. Bridgens, D. Swailes, B. Allen, S. McGough, P. Zuliani, I. D. Ofiteru, D. Wilkinson, J. Chen, T. Curtis
PLOS ONE 12(8): e0181965, 2017.
 Annotation of rulebased models with formal semantics to enable creation, analysis, reuse and visualisation [doi]
G. Misirli, M. Cavaliere, W. Waites, M. Pocock, C. Madsen, O. Gilfellon, R. HonoratoZimmer, P. Zuliani, V. Danos, A. Wipat
Bioinformatics 32(6):908917, 2016.
 Statistical Model Checking for Biological Applications [pdf]
P. Zuliani
Software Tools for Technology Transfer 17(4):527536, 2015.
 Probabilistic latent semantic analysis applied to whole bacterial genomes identifies common genomic features [pdf]
J. Rusakovica, J. Hallinan, A. Wipat, P. Zuliani
Journal of Integrative Bioinformatics 11(2):243, 2014.
 Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification [pdf]
P. Zuliani, A. Platzer, E. M. Clarke
Formal Methods in System Design 43(2):338367, 2013.
 Model checking of a synchronous diabetescancer logical network [pdf]
H. Gong, P. Zuliani, E. M. Clarke
Current Bioinformatics 8(1):915, 2013.
 Analysis and Verification of the HMGB1 Signaling Pathway [doi]
H. Gong, P. Zuliani, A. Komuravelli, J. R. Faeder, E. M. Clarke
BMC Bioinformatics 2010, 11(Suppl 7):S10. (Best Paper Award at InCoB 2010.)
 Reasoning about faulty quantum programs [pdf]
P. Zuliani
Acta Informatica 46(6):403432, 2009.
 Compiling quantum programs [pdf]
P. Zuliani
Acta Informatica 41(78):435474, 2005.
 An empirical exploration of the distributions of the Chidamber and Kemerer objectoriented metrics suite [doi]
G. Succi, W. Pedrycz, S. Djokic, P. Zuliani, B. Russo
Empirical Software Engineering 10(1):81104, 2005.
 Logical reversibility [pdf]
P. Zuliani
IBM Journal of Research and Development 45(6):807818, 2001.
Conferences
 TCount Optimizing Genetic Algorithm for Quantum State Preparation [arXiv]
A. Wright, M. Lewis, P. Zuliani, S. Soudjani
Accepted at QSW 2024: 3rd IEEE International Conference on Quantum Software.
 Automated Verification of Silq Quantum Programs using SMT Solvers [arXiv]
M. Lewis, P. Zuliani, S. Soudjani
Accepted at QSW 2024: 3rd IEEE International Conference on Quantum Software.
 Safe Reach Set Computation via Neural Barrier Certificates [arXiv]
A. Abate, S. Bogomolov, A. Edwards, K. Potomkin, S. Soudjani, P. Zuliani
Accepted at ADHS 2024: 8th IFAC Conference on Analysis and Design of Hybrid Systems.
 Verification of Quantum Systems using Barrier Certificates [arXiv] [doi]
M. Lewis, P. Zuliani, S. Soudjani
In QEST 2023: 20th International Conference on Quantitative Evaluation of SysTems. LNCS volume 14287.

Barrier Certificates for a Computational Model of Epileptic Seizures [doi]
J.F. Ingham, Y. Wang, P. Zuliani, S. Soudjani.
In 2023 IEEE International Conference on Systems, Man, and Cybernetics (SMC). IEEE, pp. 47284733, 2023.
 Modelling and Optimisation of a DNA Stack NanoDevice Using Probabilistic Model Checking [doi]
B. Li, N. Mackenzie, B. ShirtEdiss, N. Krasnogor, P. Zuliani.
In DNA28: 28th International Conference on DNA Computing and Molecular Programming. LIPIcs volume 238, pp. 5:15:22, 2022.
 Spatiotemporal model checking for 3D individualbased biofilm simulations [pdf]
B. Li, J. P. Gedara, Y. Xia, T. P. Curtis, P. Zuliani.
In DataMod 2021: 10th Symposium on From Data to Models and Back. LNCS volume 13268, pp. 157–174 2022.
 Approximate Probabilistic Reachability for Uncertain Stochastic Hybrid Systems via Gaussian Processes [pdf]
M. Vasileva, F. Shmarov, P. Zuliani
In MEMOCODE 2020: 18th ACMIEEE International Conference on Formal Methods and Models for System Design. IEEE, pp. 111, 2020.
 An Evaluation of Estimation Techniques for Probabilistic Verification [pdf]
M. Vasileva, P. Zuliani
In VECoS 2020: 14th International Conference on Verification and Evaluation of Computer and Communication Systems. LNCS volume 12519, pp. 165179, 2020.
 ARCHCOMP20 Category Report: Stochastic Models [doi]
A. Abate, H. Blom, N. Cauchi, J. Delicaris, A. Hartmanns, M. Khaled, A. Lavaei, C. Pilch, A. Remke,
S. Schupp, F. Shmarov, S. Soudjani, A. P. Vinod, B. Wooding, M. Zamani, and P. Zuliani
In ARCH20: 7th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC volume 74, pp. 76106, 2020.
 Stochastic Rate Parameter Inference using the CrossEntropy Method
[doi]
[tool page]
J. Revell, P. Zuliani
In CMSB 2018: 16th International Conference on Computational Methods in Systems Biology.
LNCS volume 11095, pp. 146164, 2018.
 Entangλe: A Translation Framework from Quipper Programs to Quantum Markov Chains [pdf]
L. Anticoli, C. Piazza, L. Taglialegne, P. Zuliani
In InfQ 2017: 7th Workshop on Quantitative Methods in Informatics. Springer CCIS, volume 825, pp. 113126, 2017.
 SMTbased Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems [pdf]
F. Shmarov, N. Paoletti, E. Bartocci, S. Lin, S. A. Smolka, P. Zuliani
In HVC 2017: 13th Haifa Verification Conference. LNCS volume 10629, pp. 131146, 2017.
 Probabilistic Hybrid Systems Verification via SMT and Monte Carlo Techniques [pdf]
F. Shmarov, P. Zuliani
In HVC 2016: 12th Haifa Verification Conference. LNCS volume 10028, pp. 152168, 2016.
 Highlevel modeling and verification of cellular signaling [doi]
N. MiskovZivanov, P. Zuliani, Q. Wang, E. M. Clarke, J. R. Faeder
In HLDVT 2016: 18th IEEE International High Level Design Validation and Test Workshop. IEEE, pp. 162169, 2016.
 Verifying Quantum Programs: From Quipper Circuits to QPMC [pdf]
L. Anticoli, C. Piazza, L. Taglialegne, P. Zuliani
In RC 2016: 8th Conference on Reversible Computation. LNCS volume 9720, pp. 213219, 2016.
 SMTBased Reasoning for Uncertain Hybrid Domains [pdf]
F. Shmarov, P. Zuliani
In AAAI16 Workshop on Planning for Hybrid Systems, 30th AAAI Conference on Artificial Intelligence, 2016.
 BioPSy: An SMTbased Tool for Guaranteed Parameter Set Synthesis of Biological Models [pdf] [tool page]
C. Madsen, F. Shmarov, P. Zuliani
In CMSB 2015: 13th Conference on Computational Methods in Systems Biology. LNCS volume 9308, pp. 182194, 2015.
 SReach: A Bounded Model Checker for Stochastic Hybrid Systems [pdf] [tool page]
Q. Wang, P. Zuliani, S. Kong, S. Gao, E. M. Clarke
In CMSB 2015: 13th Conference on Computational Methods in Systems Biology. LNCS volume 9308, pp. 1527, 2015.
 ProbReach: Verified Probabilistic DeltaReachability for Stochastic Hybrid Systems [pdf] [tool page]
F. Shmarov, P. Zuliani
In HSCC 2015: 18th International Conference on Hybrid Systems: Computation and Control. ACM, pp. 134139, 2015.
 Towards Personalized Prostate Cancer Therapy Using DeltaReachability Analysis [pdf]
B. Liu, S. Kong, S. Gao, P. Zuliani, E. M. Clarke
In HSCC 2015: 18th International Conference on Hybrid Systems: Computation and Control. ACM, pp. 227232, 2015.
 Parameter Synthesis for Cardiac Cell Hybrid Models Using DeltaDecisions [pdf]
B. Liu, S. Kong, S. Gao, P. Zuliani, E. M. Clarke
In CMSB 2014: 12th Conference on Computational Methods in Systems Biology. LNCS volume 8859, pp. 99113, 2014.
 Studies of biological networks with statistical model checking: application to immune system cells [doi]
N. MiskovZivanov, P. Zuliani, E. M. Clarke, J. R. Faeder
In ACMBCB 2013: ACM Conference on Bioinformatics, Computational Biology and Biomedical Informatics. (Poster)
 Statistical model checking for Markov decision processes [pdf]
[tool page]
D. Henriques, J. Martins, P. Zuliani, A. Platzer, E. M. Clarke
In QEST 2012: 9th International Conference on Quantitative Evaluation of SysTems. IEEE, pp. 8493.
 Model checking for studying timing of events in T cell differentiation [pdf]
P. Zuliani, N. MiskovZivanov, J. R. Faeder, E. M. Clarke
In IWBDA 2012: 4th International Workshop on BioDesign Automation, with 49th ACM/EDAC/IEEE Design Automation Conference (Abstract).
 RareEvent Verification for Stochastic Hybrid Systems [pdf]
P. Zuliani, C. Baier, E.M. Clarke
In HSCC 2012: 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 217226, 2012.
 Formal Analysis for Logical Models of Pancreatic Cancer [pdf]
H. Gong, P. Zuliani, Q. Wang, E. M. Clarke
In CDCECC 2011: 50th IEEE Conference on Decision and Control and European Control Conference. IEEE, pp. 48554860, 2011.
 Statistical Model Checking for CyberPhysical Systems [pdf]
E. M. Clarke, P. Zuliani
In ATVA 2011: 9th International Symposium on Automated Technology for Verification and Analysis. LNCS volume 6996, pp. 112, 2011. (Invited paper.)
 Model Checking of a DiabetesCancer Model [pdf]
H. Gong, P. Zuliani, E. M. Clarke
In CMLS 2011: 3rd International Symposium on Computational Models for Life Sciences, AIP Conf. Proc. 1371, pp. 234243, 2011.
 Symbolic Model Checking of Signaling Pathways in Pancreatic Cancer [pdf]
H. Gong, Q. Wang, P. Zuliani, J. R. Faeder, M. T. Lotze, E. M. Clarke
In BiCoB 2011: 3rd International Conference on Bioinformatics and Computational Biology, March 2325, 2011, New Orleans, LA.
 Analog Circuit Verification by Statistical Model Checking [pdf]
Y.C. Wang, A. Komuravelli, P. Zuliani, E. M. Clarke
In ASPDAC 2011: 16th Asia and South Pacific Design Automation Conference. IEEE, pp. 16, 2011. (Best Paper Award nomination.)
 Statistical Verification of Probabilistic Properties with Unbounded Until [pdf]
H. L. S. Younes, E. M. Clarke, P. Zuliani
In SBMF 2010: 13th Brazilian Symposium on Formal Methods. LNCS volume 6527, pp. 144160, 2011.
 Computational Modeling and Verification of Signaling Pathways in Cancer [pdf]
H. Gong, P. Zuliani, A. Komuravelli, J. R. Faeder, E. M. Clarke
In ANB 2010: 4th International Conference on Algebraic and Numeric Biology. LNCS volume 6479, pp. 117135, 2010.
 Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification [pdf]
P. Zuliani, A. Platzer, E. M. Clarke
In HSCC 2010: 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 243252, 2010.
 A Bayesian approach to model checking biological systems [pdf]
S. K. Jha, E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, P. Zuliani
In CMSB 2009: 7th Conference on Computational Methods in Systems Biology. LNCS volume 5688, pp. 218234, 2009.
 A formal derivation of Grover's quantum search algorithm [pdf]
P. Zuliani
In TASE 2007: 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, pp. 6774, 2007.
 Quantum programming with mixed states [pdf]
P. Zuliani
In QPL 2005: 3rd International Workshop on Quantum Programming Languages. ENTCS, volume 170, pp. 185199, 2007.
 On counterfactual computation [pdf]
P. Zuliani
In UC 2005: 4th International Conference on Unconventional Computation. LNCS, volume 3699, pp. 251266, 2005.
 On the transition to an open source solution for desktop automation [doi]
B. Rossi, B. Russo, P. Zuliani, G. Succi
In TCGOV 2005: ESFTCD Conference on eGovernment. LNCS, volume 3416, pp. 277285, 2005.
 Nondeterministic quantum programming [pdf]
P. Zuliani
In QPL 2004: 2nd International Workshop on Quantum Programming Languages, pp. 179195. TUCS Publication 33, Turku, Finland, 2004.
 An empirical analysis on the discontinuous use of pair programming [doi]
A. Janes, B. Russo, P. Zuliani, G. Succi
In XP 2003: 4th International Conference on eXtreme Programming and Agile Processes in Software Engineering. LNCS, volume 2675, pp. 205214, 2003.
 Quantum programming [pdf]
J. W. Sanders, P. Zuliani
In MPC 2000: Mathematics of Program Construction. LNCS, volume 1837, pp. 8099, 2000.
Edited Volumes
 Automated Reasoning for Systems Biology and Medicine [doi]
P. Liò and P. Zuliani (Editors). Springer, 2019.
Home