Mirco Giacobbe

I am a postdoc in the Systems Verification and Control and Verification groups, at the University of Oxford. I am interested in formal methods for safe artificial intelligence and symbolic and neuro-symbolic methods for the analysis of soft­ware and cyber-physical systems. Here's my CV and here's a picture of me.


Department of Computer Science, University of Oxford
Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

Selected Publications

Artificial Intelligence

Verifying Reinforcement Learning up to Infinity. Edoardo Bacci, Mirco Gia­cob­be, David Parker. IJCAI, 2021. [paper]

Shielding Atari Games with Bounded Prescience. Mirco Giacobbe, Moham­madhosein Hasanbeig, Daniel Kroening, Hjalmar Wijk. AAMAS, 2021. [paper]

How Many Bits Does it Take to Quantize Your Neural Network? Mirco Gia­cob­be, Thomas A. Henzinger, and Mathias Lechner. TACAS, 2020.   [paper]

Cyber-physical Systems

Formal Synthesis of Lyapunov Neural Networks. Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. IEEE L-CSS, 2021.   [paper]

Continuous-Time Models for System Design and Analysis. Rajeev Alur, Mirco Giacobbe, Thomas A. Henzinger, Kim G. Larsen, Marius Mikucionis. Com­pu­ting and Soft­ware Sci­ence, 2019.   [paper]

Space-time Interpolants. Goran Frehse, Mirco Giacobbe, and Thomas A. Hen­zin­ger. CAV, 2018.   [paper]

Counterexample-guided Refinement of Template Polyhedra. Sergiy Bo­go­mo­lov, Goran Frehse, Mirco Giacobbe, and Thomas A. Henzinger. TACAS, 2017.   [paper] [tech. details]

Programming Languages

Learning Probabilistic Termination Proofs. Alessandro Abate, Mirco Gia­cob­be, and Diptarko Roy. CAV, 2021   [paper]

Neural Termination Analysis. Mirco Giacobbe, Daniel Kroening, and Julian Parsert. arXiv, 2021   [preprint]

Systems Biology

Model checking Gene Regulatory Networks (best paper award). Mirco Gia­cob­be, Ashutosh Gupta, Calin Č. Guet, Thomas A. Henzinger, Tiago Paixão, and Tatjana Petrov. TACAS, 2015.   [artifact] [paper] [extended paper]