My work broadly concerns reasoning about computer systems,
in order to verify their
properties.
In particular, I work on
logic-based specification and verification of systems and programs.
Research topics
- Specifying and verifying systems
- Designing languages and tools to model systems
- Model checking
- Systems which are composed of features, and analysing feature interactions (more...)
- Reasoning about computer security
- Logic
- All kinds of logic, such as first-order logic, temporal logic and modal logic
- Applications of logic in artificial intelligence
- Belief revision
- Non-monotonic reasoning
Recent and current collaborators
- Aybek Mukhamedov
- Hasan Qunoo, University of Birmingham
- Tien Tuan Anh Dinh
- Myrto Arapinis, University of Birmingham
- Tom Chothia, University of Birmingham
- Eike Ritter, University of Birmingham
- Graham Steel, École Normale Supérieure de Cachan, France
- Ben Smyth
- King Ables
- Liqun Chen, HP Labs, UK
- Serdar Cabuk
- David Plaquin, HP Labs, UK
- Andrew Gordon, Microsoft Research, UK
- Nan Zhang
- Anongporn Salaiwarakul
- Nikos Gorogiannis, Queen Mary University of London
- Aidan Harding
- Glenn Bruns, Bell Labs / Lucent Technologies
- Dimitar Guelev, Bulgarian Academy of Sciences
- Steve Kremer, École
Normale Supérieure de Cachan
- Stephanie Delaune, École Normale Supérieure de Cachan, France
- Stefano Cattani, University of Birmingham
- Pierre Yves Schobbens, University of Namur, Belgium
- Alessio Lomuscio, University College, London, UK
- Franck Cassez, Nantes, France
- Michael Huth, Imperial College, London, UK
- Dieter Ehrich, Braunschweig, Germany