Systems Verification Group

About us

Bug We are interested in automated reasoning technology for the construction of systems. We are particularly interested in applying these methods to practical hardware and software im­ple­mentations given in industrial languages such as Verilog, C/C++ or Java. Read more about our work on software analysis or hardware verification.

NEW: MIT Press is now shipping the 2nd edition of the Model Checking book!
Watch the unboxing video!

NEW: Springer is now shipping the 2nd edition of the book on Decision Procedures!

Recent Publications

Group Members
PhD Students
MSc Students
Alumni Igor Zinovik, Postdoc
Thomas Witkowski, MSc ETH 2007, Thesis
Samuel Bernet, MSc ETH 2008
Raphael Mack, MSc ETH 2008, Thesis
Thomas Lenherr, MSc ETH 2008, Thesis
Sean Heelan, MSc Oxford 2009, Thesis, Hoare Project Prize
Haoxian Zhao, MSc Oxford 2009, Thesis, now at Freepoint Commodities
Gerard Basler, PhD ETH 2010, Thesis, now at Leonteq Securities
Nicolas Blanc, PhD ETH 2010, Thesis, now at Avaloq
Georg Weissenbacher, PhD Oxford 2010, Thesis, now Professor at TU Vienna
Mitra Purandare, PhD ETH 2010, Thesis, now Professor at the Ostschweizer Fachhochschule
Philipp Ruemmer, now Professor in Regensburg
Christoph Wintersteiger, PhD ETH 2011, Thesis, now at Imandra
Angelo Brillout, PhD ETH 2011, Thesis, now running a startup
Thomas Wahl, now at GrammaTech
Alastair Donaldson, now Professor at Imperial College
Jade Alglave, now at ARM and Professor at UCL
Nannan He, now Associate Professor at Minnesota State University at Mankato
Vijay Victor D'silva, PhD Oxford 2012, now at Google, Thesis
Yury Chebiryak, PhD ETH Zürich 2012, Thesis, now at Julius Bär
Ajitha Rajan, now Professor at the University of Edinburgh
Vojtech Forejt, now at Ultromics
Michael Tautschnig, now at Queen Mary, University of London, and AWS
Nassim Seghir, now at UCL
Alexander Kaiser, PhD Oxford 2013, now at Trumpf, Thesis
Leopold Haller, PhD Oxford 2014, now at agentic, Thesis
Cesar Rodriguez, now maître de conférences at Université Paris 13, and software architect at Cadence
Subodh Sharma, now Associate Professor at IIT Delhi
Hongyi Chen
Vincent Nimal, PhD Oxford 2015, now at AMD, Thesis
Matt Lewis, PhD Oxford 2015, now at Improbable, Thesis
Samuel Bucheli, now at Zühlke
Ruben Martins, now at CMU
Ashutosh Natraj, now running a startup
Saurabh Joshi, now at SupraOracles
Björn Wachter, now at CryptoStruct
Liana Hadarean, now at AWS
Alex Horn, PhD Oxford 2016, Thesis, now at Apple
Ganesh Narayanaswamy, MSc Oxford 2016
Peter Schrammel, now Lecturer at the University of Sussex and CTO at Diffblue
Marco Gorelli, MSc Oxford 2016
Issac Lam, MSc Oxford 2016
Alberto Sadde, MSc Oxford 2016, now at AiFi
David Landsberg, PhD Oxford 2017, Thesis, now at Frazer-Nash
Lihao Liang, PhD Oxford 2017, now at Google
Cristina David, now Senior Lecturer in Bristol
Pascal Kesseli, PhD Oxford 2017, Thesis, now at Meta
Rajdeep Mukherjee, PhD Oxford 2017, now at AWS, Thesis
Lucas Cordeiro, now Professor in Manchester
Daniel Poetzl, PhD Oxford 2018, Thesis
Ralph Abboud, MSc Oxford 2018, now working at Schmidt Futures
Marcelo Sousa, PhD Oxford 2018, Thesis, now at Snyk
Dario Cattaruzza, PhD Oxford 2018, Thesis, now at Sportable
Youcheng Sun, now lecturer at the University of Manchester
Sean Heelan, PhD Oxford 2020, Thesis
Hadrien Pouget, now with The Carnegie Endowment for International Peace
Hjalmar Wijk, MSc Oxford 2020, now with METR
John Galea, PhD Oxford 2021, Thesis
Mirco Giacobbe, now lecturer at the University of Birmingham
Martin Brain, now lecturer at City, University of London
Isaac Dunn, PhD Oxford 2022, now contractor for Anthropic, Thesis
Natasha Jeppu, PhD Oxford 2023, now at Amazon Web Services, Thesis
Julian Parsert, Phd Oxford 2024, Thesis

A photo taken after a group punting trip, and another taken at a CProver workshop at Chicheley Hall.

Funding


ERC

 

This project has received funding from the European Union's Seventh Framework Programme for research, technological development and demonstration under grant agreement no. 280053.