Team
The SCorCH team is spread between the University of Manchester and the University of Oxford.
Giles Reger
Giles Reger is a Senior Lecturer in the Department of Computer Science at the University of Manchester. He has joint expertise in automated reasoning and runtime verification. He is a lead developer of the Vampire theorem prover and MarQ runtime verification tool.
Tom Melham
Tom Melham is a Professor in the Department of Computer Science at the University of Oxford. He is an expert in formal hardware verification, model checking, and theorem proving.
Daniel Kroening
Daniel Kroening is a Senior Principal Scientist at Amazon Web Services and a Professor in the Department of Computer Science at the University of Oxford. He is well known for his contributions to model checking and decision procedures for automated software analysis. He leads the development of the CBMC model checker.
Lucas Corderio
Lucas Cordeiro is a Senior Lecturer in the Department of Computer Science at the University of Manchester. He has joint expertise in software model checking, automated testing, and program synthesis. He leads the development of the ESBMC model checker.
Konstantin Korovin
Konstantin Korovin is a Senior Lecturer in the Department of Computer Science at the University of Manchester. He has joint expertise in automated reasoning and hardware model checking. He leads the development of the iProver theorem prover.
Mustafa A. Mustafa
Mustafa A. Mustafa is a Dame Kathleen Ollerenshaw Research Fellow in the Department of Computer Science at The University of Manchester. His research expertise includes information security, data privacy and applied cryptography.
Fedor Shmarov
Fedor Shmarov is a Research Associate in the Department of Computer Science at The University of Manchester. His research expertise include model checking and formal verification of stochastic hybrid systems.
Ahmed Bhayat
Ahmed Bhayat is a Research Associate in the Department of Computer Science at The University of Manchester. Amongst his areas of interests are automated reasoning, lambda calculus and type theory. He is involved in the development of the Vampire theorem prover.
Franz Brauße
Franz is a Research Associate in the Department of Computer Science at the University of Manchester. His area of interest lie in computable analysis and its efficient software implementations.
Seung Hoon Park
Seung Hoon Park is a Research Assistant in the Department of Computer Science at the University of Oxford. His area of interest lies in programming languages, formal verification and model checking.
Rekha Pai
Rekha Pai is a Research Associate in the Department of Computer Science at the University of Oxford. Her primary research interest is in verification of embedded systems.
Associates
Dapeng Gao
Dapeng is a PhD candidate at the University of Cambridge and completed his Masters at the University of Oxford. During his Masters he collaborated with Tom Melham on end-to-end verification of the CHERI RISC-V processor.
Fareed Arif
Fareed is a research associate at the University of Oxford working on the related Soteria project. He has expertise in formal verification that include static and dynamic analysis techniques for validation of hardware and software systems
Kunjian Song
Kunjian is a research associate at the University of Manchester working on the related Soteria project. Prior to joining Soteria he was an engineer at ARM Cambridge and completed his MSc contributing to the ESBMC model checker.
Avi Shaked
Avi Shaked is a Senior Research Associate in the Department of Computer Science at the University of Oxford working on the related Soteria project. Avi has significant industrial and research experience in systems engineering and systems security. His research interests include systems design and domain-specific modelling.
Advisory Board
SCorCH is guided by an advisory board consisting of the following: