I am an Associate Professor at the University of Birmingham. I lead the AI Verification Group and I am the head of Zeroth Research. I develop technology to formally certify that algorithmic systems are safe and secure by combining ideas from machine learning and automated reasoning. Here's my CV and here's a picture of me.
Students interested in pursuing a PhD at the University of Birmingham in an intersection of formal methods, artificial intelligence, control theory and cybersecurity are invited to get in touch.
Contact
School of Computer Science, University of Birmingham
Edgbaston, Birmingham, B15 2TT, UK
m.giacobbe@bham.ac.uk
Selected Publications
Privacy-preserving Formal Verification
Zero-knowledge Model Checking. Pascal Berrang, Mirco Giacobbe, Jacob Swales, Xiao Yang. 2026 [preprint]
Formal Methods and Machine Learning for Cyber-physical Systems
Neural Continuous-time Supermartingale Certificates. Grigory Neustroev, Mirco Giacobbe, and Anna Lukina. AAAI, 2025 [paper]
Stochastic Omega-regular Verification and Control with Supermartingales. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. CAV, 2024 [paper] [follow-up paper]
Formal Synthesis of Lyapunov Neural Networks. Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. IEEE L-CSS, 2020. [paper]
Formal Methods and Machine Learning for Software and Hardware Systems
Neural Model Checking. Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig. NeurIPS, 2024. [paper] [follow-up paper]Learning Probabilistic Termination Proofs. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. CAV, 2021 [paper]
How Many Bits Does it Take to Quantize Your Neural Network? Mirco Giacobbe, Thomas A. Henzinger, and Mathias Lechner. TACAS, 2020. [paper]
Formal Methods for Systems Biology
Model checking Gene Regulatory Networks (best paper award). Mirco Giacobbe, Ashutosh Gupta, Calin Č. Guet, Thomas A. Henzinger, Tiago Paixão, and Tatjana Petrov. TACAS, 2015. [paper] [extended paper]