Background

Please check my up to date website https://pzuliani.github.io/.

I am a Reader in the School of Computing. Before coming to Newcastle I was at Carnegie Mellon University working with Edmund Clarke on model checking. I received my Laurea degree from the Università degli Studi di Milano (Italy) and my D.Phil. from the University of Oxford (UK), both in Computer Science.

I have been involved in several other funded projects - see https://pzuliani.github.io/ for a full list.

Areas of expertise: Verification for systems biology and cyber-physical systems; quantum computing.

Google scholar: Click here.

Research

My current research area is formal verification of biological models and cyber-physical systems, using in particular model checking and SAT/SMT solvers. I am also interested in quantum programming and reversible computation, and formal methods for the specification and derivation of code (a la Dijkstra).

My research finds application, for example, in the verification of biomedical devices (eg, artificial pancreas for treating diabetes - paper), for optimising psoriasis treatments (paper) and the simulation of complex microbial communities (eg, for wastewater treatment - paper).

With my students and collaborators we have developed several software tools to support and implement our theoretical research:

• ProbReach: Verified probabilistic bounded reachability for stochastic hybrid systems [tool page] [paper] 
• SPICE: Stochastic Parameter Inference with the Cross-Entropy Method [tool page] [paper] 
• NUFEB: Agent-based Modelling of Microbial Communities [tool page] [paper]

Teaching

I am currently teaching the MSc modules Modelling Cellular Systems (CSC8324) and Bio-Data Science (CSC8332).

Publications

• Xia Y, Jayathilake PG, Li B, Zuliani P, Deehan D, Longyear J, Stoodley P, Chen J. Coupled CFD-DEM modelling to predict how EPS affects bacterial biofilm deformation, recovery and detachment under flow conditions. Biotechnology and Bioengineering 2022, 119(9), 2551-2563.
• Shmarov F, Smith GR, Weatherhead SC, Reynolds NJ, Zuliani P. Individualised computational modelling of immune mediated disease onset, flare and clearance in psoriasis. PLoS Computational Biology 2022, 18(9), e1010267.
• Abate A, Blom H, Bouissou M, Cauchi N, Chraibi H, Delicaris J, Haesaert S, Hartmanns A, Khaled M, Lavaei A, Ma H, Mallik K, Niehage M, Remke A, Schupp S, Shmarov F, Soudjani S, Thorpe A, Turcuman V, Zuliani P. ARCH-COMP21 Category Report: Stochastic Models. In: EPiC Series in Computing. 2021, EasyChair.
• Xia Y, Jayathilake P, Li B, Zuliani P, Chen J. CFD-DEM modelling of biofilm streamer oscillations and their cohesive failure in fluid flow. Biotechnology and Bioengineering 2021, 118(2), 918-929.
• Georgopoulos K, Emary C, Zuliani P. Comparison of quantum-walk implementations on noisy intermediate-scale quantum computers. Physical Review A 2021, 103, 022408.
• Georgopoulos K, Emary C, Zuliani P. Modeling and simulating the noisy behavior of near-term quantum computers. Physical Review A 2021, 104(6), 062432.
• Watson N, Wilson N, Shmarov F, Zuliani P, Reynolds NJ, Weatherhead SC. The use of psoriasis biomarkers, including trajectory of clinical response, to predict clearance and remission duration to UVB phototherapy. Journal of the European Academy of Dermatology and Venereology 2021, 35(11), 2250-2258.
• Shmarov F, Soudjani S, Paoletti N, Bartocci E, Lin S, Smolka SA, Zuliani P. Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems. IEEE Access 2020, 8, 180825-180843.
• Vasileva M, Shmarov F, Zuliani P. Probabilistic Reachability for Uncertain Stochastic Hybrid Systems via Gaussian Processes. In: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2020). 2020, Jaipur, India (Online): IEEE.
• Oyebamiji OK, Wilkinson DJ, Li B, Jayathilake PG, Zuliani P, Curtis TP. Bayesian emulation and calibration of an individual-based model of microbial communities. Journal of Computational Science 2019, 30, 194-208.
• Gogulancea V, Gonzalez-Cabaleiro R, Li B, Taniguchi D, Jayathilake PG, Chen J, Wilkinson D, Swailes D, McGough S, Zuliani P, Ofiteru ID, Curtis T. Individual based model links thermodynamics, chemical speciation and environmental conditions to microbial growth. Frontiers in Microbiology 2019, 10, 1871.
• Jayathilake PG, Li B, Zuliani P, Curtis T, Chen J. Modelling bacterial twitching in fluid flows: a CFD-DEM approach. Scientific Reports 2019, 9, 14540.
• Li B, Taniguchi D, Pahala- Gedara J, Gogulancea V, Gonzalez-Cabaleiro R, Chen J, McGough AS, Ofiteru ID, Curtis TP, Zuliani P. NUFEB: A Massively Parallel Simulator for Individual-based Modelling of Microbial Communities. PLoS Computational Biology 2019, 15(2), e1007125.
• Grozinger L, Amos M, Gorochowski TE, Carbonell P, Oyarzún DA, Stoof R, Fellermann H, Zuliani P, Tas H, Goñi-Moreno A. Pathways to cellular supremacy in biocomputing. Nature Communications 2019, 10, 5250.
• Oyebamiji OK, Wilkinson DJ, Pahala-Gedara J, Rushton SP, Li B, Bridgens B, Zuliani P. A Bayesian approach to modelling the impact of hydrodynamic shear stress on biofilm deformation. PLOS ONE 2018, 13(4), e0195484.
• Revell J, Zuliani P. Stochastic Rate Parameter Inference Using the Cross-Entropy Method. In: 16th International Conference on Computational Methods in Systems Biology. 2018, Brno, Czech Republic: Springer, Cham.
• Jayathilake PG, Gupta P, Li B, Madsen C, Oyebamiji O, Gonzalez-Cabaleiro R, Rushton S, Bridgens B, Swailes D, Allen B, McGough AS, Zuliani P, Ofiteru ID, Wilkinson DJ, Chen J, Curtis TP. A mechanistic individual-based model of microbial communities. PLoS One 2017, 12(8), e0181965.
• Anticoli L, Piazza C, Taglialegne L, Zuliani P. Entangλe: A Translation Framework from Quipper Programs to Quantum Markov Chains. In: InfQ 2017: 7th Workshop on Quantitative Methods in Informatics. 2017, Venice, Italy: Springer.
• Shmarov F, Paoletti N, Bartocci E, Lin S, Smolka SA, Zuliani P. SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems. In: HVC 2017: Hardware and Software: Verification and Testing. 2017, Haifa, Israel: Springer Verlag.
• Misirli G, Cavaliere M, Waites W, Pocock M, Madsen C, Gilfellon O, Honorato-Zimmer R, Zuliani P, Danos V, Wipat A. Annotation of rule-based models with formal semantics to enable creation, analysis, reuse and visualisation. Bioinformatics 2016, 32(6), 908-917.
• Miskov-Zivanov N, Zuliani P, Wang QS, Clarke EM, Faeder JR. High-level modeling and verification of cellular signaling. In: 18th IEEE International High Level Design Validation and Test Workshop (HLDVT). 2016, Santa Cruz, California, USA: Institute of Electrical and Electronics Engineers.
• Shmarov F, Zuliani P. Probabilistic hybrid systems verification via SMT and Monte Carlo techniques. In: 12th Haifa Verification Conference (HVC 2016). 2016, Haifa, Israel: Springer.
• Shmarov F, Zuliani P. SMT-based reasoning for uncertain hybrid domains. In: AAAI Workshop - Technical Report. 2016, Phoenix, Arizona USA: AI Access Foundation.
• Anticoli L, Piazza C, Taglialegne L, Zuliani P. Towards Quantum Programs Verification: From Quipper Circuits to QPMC. In: 8th International Conference on Reversible Computation. 2016, Bologna, Italy: Springer.
• Madsen C, Shmarov F, Zuliani P. BioPSy: An SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models. In: 13th International Conference on Computational Methods in Systems Biology (CMSB). 2015, Nantes, France: Springer.
• Shmarov F, Zuliani P. ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems. In: 18th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). 2015, Seattle, WA, USA: ACM.
• Wang Q, Zuliani P, Kong S, Gao S, Clarke EM. SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems. In: 13th International Conference on Computational Methods in Systems Biology (CMSB). 2015, Nantes, France: Springer.
• Zuliani P. Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer 2015, 17(4), 527-536.
• Liu B, Kong S, Gao S, Zuliani P, Clarke EM. Towards personalized prostate cancer therapy using delta-reachability analysis. In: 18th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). 2015, Seattle, WA, USA: Association for Computing Machinery.
• Liu B, Kong S, Gao S, Zuliani P, Clarke EM. Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions. In: 12th International Conference on Computational Methods in Systems Biology (CMSB). 2014, Manchester, UK: Springer.
• Rusakovica J, Hallinan J, Wipat A, Zuliani P. Probabilistic Latent Semantic Analysis Applied to Whole Bacterial Genomes Identifies Common Genomic Features. Journal of Integrative Bioinformatics 2014, 11(2), 243.
• Zuliani P, Platzer A, Clarke EM. Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design 2013, 43(2), 338-367.
• Gong H, Zuliani P, Clarke EM. Model checking of a synchronous diabetes-cancer logical network. Current Bioinformatics 2013. In Press.
• Zuliani P, Miskov-Zivanov N, Faeder JR, Clarke EM. Model checking for studying timing of events in T cell differentiation. In: Fourth International Workshop on Bio-Design Automation (IWBDA). 2012, San Francisco, California, USA.
• Zuliani P, Baier C, Clarke EM. Rare-event verification for stochastic hybrid systems. In: 15th ACM international conference on Hybrid Systems: Computation and Control (HSCC). 2012, Beijing, China: ACM Press.
• Henriques D, Martins JG, Zuliani P, Platzer A, Clarke EM. Statistical model checking for Markov decision processes. In: 9th International Conference on Quantitative Evaluation of SysTems (QEST). 2012, London: IEEE.
• Wang YC, Komuravelli A, Zuliani P, Clarke EM. Analog circuit verification by statistical model checking. In: 16th Asia and South Pacific Design Automation Conference (ASP-DAC). 2011, Yokohama, JAPAN: IEEE.
• Gong H, Zuliani P, Wang Q, Clarke EM. Formal analysis for logical models of pancreatic cancer. In: 50th IEEE Conference of Decision and Control (CDC)/European Control Conference (ECC). 2011, Orlando, FL: IEEE.
• Gong H, Zuliani P, Clarke EM. Model checking of a diabetes-cancer model. In: International Symposium on Computational Models for Life Sciences (CMLS-11). 2011, Toyama City, Japan: AIP.
• Clarke EM, Zuliani P. Statistical model checking for cyber-physical systems. In: 9th International Symposium on Automated Technology for Verification and Analysis (ATVA). 2011, Taipei, Taiwan: Springer-Verlag Berlin.
• Gong H, Wang Q, Zuliani P, Faeder JR, Lotze MT, Clarke EM. Symbolic model checking of signaling pathways in pancreatic cancer. In: 3rd International Conference on Bioinformatics and Computational Biology, BICoB-2011. 2011, New Orleans, Louisiana, USA: ISCA.
• Gong H, Zuliani P, Komuravelli A, Faeder JR, Clarke EM. Analysis and verification of the HMGB1 signaling pathway. BMC Bioinformatics 2010, 11(suppl. 7), S10.
• Zuliani P, Platzer A, Clarke EM. Bayesian statistical model checking with application to Simulink/Stateflow verification. In: HSCC 2010: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. 2010, Stockholm, Sweden: ACM.
• Gong H, Zuliani P, Komuravelli A, Faeder JR, Clarke EM. Computational modeling and verification of signaling pathways in cancer. In: ANB. 2010.
• Younes HLS, Clarke EM, Zuliani P. Statistical verification of probabilistic properties with unbounded Until. In: SBMF 2010: 13th Brazilian Symposium on Formal Methods. 2010, Natal, Brazil: Springer.
• Jha S, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P. A Bayesian Approach to Model Checking Biological Systems. In: Computational Methods in Systems Biology: 7th International Conference, CMSB 2009. 2009, Bologna, Italy: Springer-Verlag.
• Zuliani P. Reasoning about faulty quantum programs. Acta Informatica 2009, 46(6), 403-432.
• Zuliani P. A formal derivation of Grover's quantum search algorithm. In: 1st Joint Symposium on Theoretical Aspects of Software Engineering (TASE). 2007, IEEE.
• Succi G, Pedrycz W, Djokic S, Zuliani P, Russo B. An Empirical Exploration of the Distributions of theChidamber and Kemerer Object-Oriented Metrics Suite. Empirical Software Engineering 2005, 10(1), 81-104.
• Zuliani P. Compiling quantum programs. Acta Informatica 2005, 41(7-8), 435-474.
• Zuliani P. On counterfactual computation. In: Unconventional Computation: 4th International Conference (UC 2005). 2005, Sevilla, Spain: Springer.
• Zuliani P. Quantum programming with mixed states. In: 3rd International Workshop on Quantum Programming Languages (QPL 2005). 2005, Chicago, Ill.
• Zuliani P. Non-deterministic quantum programming. In: 2nd International Workshop on Quantum Programming Languages (QPL). 2004, Turku, Finland: Turku Centre for Computer Science.
• Zuliani P. Logical Reversibility. IBM Journal of Research and Development 2001, 45(6), 807-818.
• Sanders JW, Zuliani P. Quantum programming. In: MPC. 2000.