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 Agent-Based 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. Fuentes-Cabrera. 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. 4-10, 2011. LNCS volume 7682, pp. 1-30, 2012.

• Transcriptomic profiling and machine learning uncover gene signatures of psoriasis endotypes and disease severity [doi]
  A. Rider, H. J. Grantham, G. R. Smith, D. S. Watson, J. Casement, S. J. Cockell, J. Gisby, A. C. Foulkes, R. Henkin, W. A. Iqbal, T. Ewen, S. Amarnath, S. Ng, P. Zuliani, N. Dand, D. Stocken, C. Traini, E. Thomas, S. Kalyana-Sundaram, D. K. Rajpal, K. M. Smith, J. N. Barker, C. E. M. Griffiths, P. Di Meglio, C. H. Smith, R. B. Warren, M. R. Barnes & N. J. Reynolds
  Nature Communications Medicine 6, 65, 2026.
• Cooperation between autotrophic and heterotrophic denitrifiers under low C/N ratios revealed by individual-based 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 light-driven microbial community [doi]
  J. K. Sakkos, M. Santos-Merino, E. J. Kokarakis, B. Li, M. Fuentes-Cabrera, 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 CFD-DEM 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, 2551-2563, 2022.
• Modelling and Simulating the Noisy Behaviour of Near-term 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: 2250-2258, 2021
  
• A Comparison of Quantum Walk Implementations on Noisy Intermediate-Scale Quantum Computers [arXiv]
  K. Georgopoulos, C. Emary, P. Zuliani
  Physical Review A 103, 022408, 2021.
• CFD-DEM 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 Sampled-Data Stochastic Nonlinear Systems [doi]
  F. Shmarov, S. Soudjani, N. Paoletti, E. Bartocci, S. Lin, S. A. Smolka, P. Zuliani
  IEEE Access 8:180825-180843, 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. Goni-Moreno
  Nature Communications 10, 5250 (2019).
• NUFEB: A Massively Parallel Simulator for Individual-based Modelling of Microbial Communities [doi]
  B. Li, D. Taniguchi, J. P. Gedara, V. Gogulancea, R. Gonzalez-Cabaleiro, 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 CFD-DEM 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. Gonzalez-Cabaleiro, 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 individual-based model of microbial communities [doi]
  O. Oyebamiji, D. Wilkinson, B. Li, P. G. Jayathilake, P. Zuliani, T. P. Curtis
  Journal of Computational Science 30:194-208, 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 Individual-based Model of Microbial Communities [doi]
  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
  PLOS ONE 12(8): e0181965, 2017.
• Annotation of rule-based 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. Honorato-Zimmer, P. Zuliani, V. Danos, A. Wipat
  Bioinformatics 32(6):908-917, 2016.
• Statistical Model Checking for Biological Applications [pdf]
  P. Zuliani
  Software Tools for Technology Transfer 17(4):527-536, 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):338-367, 2013.
• Model checking of a synchronous diabetes-cancer logical network [pdf]
  H. Gong, P. Zuliani, E. M. Clarke
  Current Bioinformatics 8(1):9-15, 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):403-432, 2009.
• Compiling quantum programs [pdf]
  P. Zuliani
  Acta Informatica 41(7-8):435-474, 2005.
• An empirical exploration of the distributions of the Chidamber and Kemerer object-oriented metrics suite [doi]
  G. Succi, W. Pedrycz, S. Djokic, P. Zuliani, B. Russo
  Empirical Software Engineering 10(1):81-104, 2005.
• Logical reversibility [pdf]
  P. Zuliani
  IBM Journal of Research and Development 45(6):807-818, 2001.

Conferences (with acceptance rate where available)

• A Hybrid Classical-Quantum Annealing Algorithm for the TSP [arXiv]
  S. Hu, V. Lopata, S. Sinno, S. Thuravakkath, P. Zuliani
  Accepted at the 5th Quantum Optimization workshop, GECCO 2026 (28th Genetic and Evolutionary Computation Conference).
• LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [arXiv]
  E. Casablanca, O. Schön, P. Zuliani, S. Soudjani
  Accepted at AAAI-26 (40th Annual AAAI Conference on Artificial Intelligence).
  (Acceptance rate: 17.6%)
• Barrier Certificate Computation using Gaussian Process Optimization [pdf]
  X. Ge, S. Soudjani, P. Zuliani
  Accepted at the 2025 Workshop on Awareness in Learning Agents (ALA).
• Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach [arXiv]
  S. Hu, V. Lopata, S. Soudjani, P. Zuliani
  Accepted at QSW 2025 (4th IEEE International Conference on Quantum Software).
  (Acceptance rate: 22.8%)
• High-level quantum algorithm programming using Silq [arXiv]
  V. Bezganovic, M. Lewis, S. Soudjani, P. Zuliani
  Accepted at QUASAR 2025 (2nd Workshop on Quantum Algorithms, Software and Applied Research).
• T-Count Optimizing Genetic Algorithm for Quantum State Preparation [arXiv] [doi]
  A. Wright, M. Lewis, P. Zuliani, S. Soudjani
  Accepted at QSW 2024: 3rd IEEE International Conference on Quantum Software.
  (Acceptance rate: 25.6%)
• Automated Verification of Silq Quantum Programs using SMT Solvers [arXiv] [doi]
  M. Lewis, P. Zuliani, S. Soudjani
  Accepted at QSW 2024: 3rd IEEE International Conference on Quantum Software.
  (Acceptance rate: 25.6%)
• Safe Reach Set Computation via Neural Barrier Certificates [arXiv] [doi]
  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.
  (Acceptance rate: 52.2%)
  
• 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. 4728-4733, 2023.
• Modelling and Optimisation of a DNA Stack Nano-Device Using Probabilistic Model Checking [doi]
  B. Li, N. Mackenzie, B. Shirt-Ediss, N. Krasnogor, P. Zuliani.
  In DNA28: 28th International Conference on DNA Computing and Molecular Programming. LIPIcs volume 238, pp. 5:1-5:22, 2022.
  (Acceptance rate: 64%)
  
• Spatio-temporal model checking for 3D individual-based 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. (Invited paper)
• Approximate Probabilistic Reachability for Uncertain Stochastic Hybrid Systems via Gaussian Processes [pdf]
  M. Vasileva, F. Shmarov, P. Zuliani
  In MEMOCODE 2020: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. IEEE, pp. 1-11, 2020.
  (Acceptance rate: 53%)
  
• 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. 165-179, 2020.
  (Acceptance rate: 33.3%)
• ARCH-COMP20 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. 76-106, 2020.
• Stochastic Rate Parameter Inference using the Cross-Entropy Method [doi] [tool page]
  J. Revell, P. Zuliani
  In CMSB 2018: 16th International Conference on Computational Methods in Systems Biology. LNCS volume 11095, pp. 146-164, 2018.
  (Acceptance rate: 47.8%)
  
• 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. 113-126, 2017.
• SMT-based 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. 131-146, 2017.
  (Acceptance rate: 48.8%)
• 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. 152-168, 2016.
  (Acceptance rate: 50%)
• High-level modeling and verification of cellular signaling [doi]
  N. Miskov-Zivanov, 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. 162-169, 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. 213-219, 2016.
  (Acceptance rate: 60.5%)
• SMT-Based Reasoning for Uncertain Hybrid Domains [pdf]
  F. Shmarov, P. Zuliani
  In AAAI-16 Workshop on Planning for Hybrid Systems, 30th AAAI Conference on Artificial Intelligence, 2016.
• BioPSy: An SMT-based 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. 182-194, 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. 15-27, 2015.
• ProbReach: Verified Probabilistic Delta-Reachability 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. 134-139, 2015.
• Towards Personalized Prostate Cancer Therapy Using Delta-Reachability 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. 227-232, 2015.
• Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions [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. 99-113, 2014.
• Studies of biological networks with statistical model checking: application to immune system cells [doi]
  N. Miskov-Zivanov, P. Zuliani, E. M. Clarke, J. R. Faeder
  In ACM-BCB 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. 84-93.
• Model checking for studying timing of events in T cell differentiation [pdf]
  P. Zuliani, N. Miskov-Zivanov, J. R. Faeder, E. M. Clarke
  In IWBDA 2012: 4th International Workshop on Bio-Design Automation, with 49th ACM/EDAC/IEEE Design Automation Conference (Abstract).
• Rare-Event 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. 217-226, 2012.
• Formal Analysis for Logical Models of Pancreatic Cancer [pdf]
  H. Gong, P. Zuliani, Q. Wang, E. M. Clarke
  In CDC-ECC 2011: 50th IEEE Conference on Decision and Control and European Control Conference. IEEE, pp. 4855-4860, 2011.
• Statistical Model Checking for Cyber-Physical Systems [pdf]
  E. M. Clarke, P. Zuliani
  In ATVA 2011: 9th International Symposium on Automated Technology for Verification and Analysis. LNCS volume 6996, pp. 1-12, 2011. (Invited paper.)
• Model Checking of a Diabetes-Cancer 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. 234-243, 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 23-25, 2011, New Orleans, LA.
• Analog Circuit Verification by Statistical Model Checking [pdf]
  Y.-C. Wang, A. Komuravelli, P. Zuliani, E. M. Clarke
  In ASP-DAC 2011: 16th Asia and South Pacific Design Automation Conference. IEEE, pp. 1-6, 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. 144-160, 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. 117-135, 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. 243-252, 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. 218-234, 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. 67-74, 2007.
• Quantum programming with mixed states [pdf]
  P. Zuliani
  In QPL 2005: 3rd International Workshop on Quantum Programming Languages. ENTCS, volume 170, pp. 185-199, 2007.
• On counterfactual computation [pdf]
  P. Zuliani
  In UC 2005: 4th International Conference on Unconventional Computation. LNCS, volume 3699, pp. 251-266, 2005.
• On the transition to an open source solution for desktop automation [doi]
  B. Rossi, B. Russo, P. Zuliani, G. Succi
  In TCGOV 2005: ESF-TCD Conference on e-Government. LNCS, volume 3416, pp. 277-285, 2005.
• Non-deterministic quantum programming [pdf]
  P. Zuliani
  In QPL 2004: 2nd International Workshop on Quantum Programming Languages, pp. 179-195. 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. 205-214, 2003.
• Quantum programming [pdf]
  J. W. Sanders, P. Zuliani
  In MPC 2000: Mathematics of Program Construction. LNCS, volume 1837, pp. 80-99, 2000.

Edited Volumes

• Automated Reasoning for Systems Biology and Medicine [doi]
  P. Liò and P. Zuliani (Editors). Springer, 2019.