Systems Verification Group

About us

Bug We are interested in formal methods for the correct construction of hardware and soft­ware systems. Our focus is on automated methods for checking compliance of an implementation with a specification, and in particular Model Checking.

We are particularly interested in applying these methods to practical hardware and software im­ple­mentations given in industrial languages such as Verilog, C or C++. Read more about software verif­ication or hardware verification.

NEW: FLOC 2018 will be in Oxford!

Submit to FMSD!

Recent Publications

Group Members
Staff Martin Brain
Cristina David
Daniel Kroening
Peter Schrammel
PhD Students Dario Cattaruzza
Pascal Kesseli
David Landsberg
Lihao Liang
Rajdeep Mukherjee
Daniel Neville
Ganesh Narayanaswamy
Daniel Poetzl
Marcelo Sousa
MSc Students
Alumni Igor Zinovik, Postdoc
Thomas Witkowski, MSc 2007, Thesis
Samuel Bernet, MSc 2008
Raphael Mack, MSc 2008, Thesis
Thomas Lenherr, MSc 2008, Thesis
Sean Heelan, MSc 2009, Thesis, Hoare Project Prize, now with Persistence Labs
Haoxian Zhao, MSc 2009, Thesis, now at JP Morgan
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 at TU Vienna
Mitra Purandare, PhD ETH 2010, Thesis, now at IBM Research
Philipp Ruemmer, now Assistant Professor in Uppsala
Christoph Wintersteiger, PhD ETH 2011, Thesis, now at Microsoft Research
Angelo Brillout, PhD ETH 2011, Thesis
Thomas Wahl, now at Northeastern University, Boston
Alastair Donaldson, now Senior Lecturer at Imperial College
Jade Alglave, now at UCL and Microsoft Research
Nannan He, now at Minnesota State University at Mankato
Vijay Victor D'silva, PhD Oxford 2012, now at Google
Yury Chebiryak, PhD ETH Zürich 2012, Thesis, now at Amplitude Capital
Ajitha Rajan, now Lecturer at the University of Edinburgh
Vojtech Forejt, now Associate Professor in the CS Department
Michael Tautschnig, now at Queen Mary, University of London
Nassim Seghir, now at the University of Edinburgh
Alexander Kaiser, PhD Oxford 2013, Thesis
Leopold Haller, PhD Oxford 2014, now at Google
Cesar Rodriguez, now maître de conférences at Université Paris 13
Subodh Sharma, now at IIT Delhi
Hongyi Chen
Vincent Nimal, PhD Oxford 2015, now at MSR Redmond, Thesis
Matt Lewis, PhD Oxford 2015, now at Improbable
Samuel Bucheli, now at Zühlke
Ruben Martins, now at UT Austin
Ashutosh Natraj, now running a startup
Saurabh Joshi, now Assistant Professor at IIT Guwahati
Björn Wachter, now at SSW Trading
Liana Hadarean, now at Coverity
Alex Horn, now at Fujitsu Labs

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