School of Computer Science

Telephone: +44 (0) 121 41-48819
Email:

News

16/11/2009: Lecture on November 23 is CANCELLED
14/11/2009: I co-organise 50 Years of Computer Science in Birmingham
01/11/2009: This week I will give seminars at INRIA, Saclay and PPS, Paris
06/10/2009: New lecture time for CUDA module: Monday 9-11, UG40, Computer Science
05/10/2009: New web page for CUDA module
27/09/2009: Remedial maths for incoming students
24/09/2009: New doctoral student starting, Alex Smith
22/09/2009: Synchron 2009 will be held in Dagstuhl
07/09/2009: PC member for LICS 2010
22/08/2009: Lics tutorial paper Applications of Game Semantics: From Software Analysis to Hardware Synthesis is available online
22/08/2009: Lics paper, with Adam Bakewell, Clipping: A Semantics-Directed Syntactic Approximation is available online
22/08/2009: paper on function interface models was mentioned on Lambda the Ultimate
13/08/2009: an N-Category Cafe comment on my hardware compilation work
04/07/2009: most slides from the Bridging the Gap workshop are online

Older events

22/06/2009: Technology Strategy Board workshop on The Future of Multicore Computing in the UK
04/06/2009: Preliminary LICS programme posted
03/06/2009: Upcoming workshop in Birmingham: The Programming Challenge of Heterogeneous Architectures
15/05/2009: Teaching new module in Autum 2009, Programming Massively Parallel Architectures
12/05/2009: Upcoming Seminar at University of Ghent, on 26-27 May
09/04/2009: Tacas '09 paper Compositional Predicate Abstraction from Game Semantics (Bakewell, Ghica) posted online
19/03/2009: upcoming paper at LICS'09: Clipping: A Semantics-directed syntactic approximation, with Adam Bakewell
25/02/2009: upcoming talks at GALOP for myself, my postdoc Adam Bakewell and my student Mohamed Menaa
20/02/2009: series of three lectures at the University of Bucharest on game semantics and applications to verification and synthesis (in Romanian)
04/02/2009: registration for the Games for Logic and Programming Languages IV (GALOP) workshop is now open.
14/12/2008: upcoming new paper with Adam Bakewell, Compositional Predicate Abstraction from Game Semantics; to appear at TACAS'09.
04/12/2008: new paper, Function Interface Models for Hardware Compilation, belabors an obvious point.
03/12/2008: PC of OpenCert at ETAPS 09.
01/12/2008: talk at Synchron'08
22/11/2008: upcoming tutorial on applications of game semantics at LICS'09
21/11/2008: upcoming (with Peter O'Hearn) special session dedicated to Bob Tennent at MFPS 25
16/09/2008: PC of Automatic Program Verification
07/07/2008: PC of TLCA 2009.
09/06/2008: PC of GlobalComp (a Synasc workshop)
26/05/2008: I will no longer have regular office hours. Please email to make an appointment.
21/05/2008: The submission site for the APAL special issue associated with GALOP III is now open;
14/05/2008: PC for OpenCert/FLOSS;
09/05/2008: GaLoP IV will be a part of ETAPS 2009;
09/04/2008: course on Games for Software Verification at MGS 2008;
08/04/2008: The book Moisil and His Followers is now in print;
03/03/2008: The GaLoP III programme is now on-line; register here.
21/02/2008: departmental seminar at Univerisity of Warwick on A structured approach to VLSI design;
06/02/2008: The APAL special issue on GaLoP I is now available in print.
09/01/2008: During the Spring term I will teach part of the Automatic Verification module
09/01/2008: My new office hour for the Spring term is Tuesday, 2.30 - 3.30;
10/12/2007: A paper describing Mage was accepted for publication at TACAS 2008: On-the-Fly Techniques for Games-Based Software Model Checking (with Adam Bakewell)
18/12/2007: talk at the MGS Chrismas seminar: Geometry of Synthesis
06/11/2007: seminar at Oxford University Computing Lab: Lazy games-based software model checking
24/10/2007: seminar at Imperial College, Electrical Engineering: Yet another C-to-hardware compiler

Research interests

I am interested in game semantics and its applications: program verification, program analysis, specification logics, hardware synthesis.

If you are interested in doing a PhD in this area you should read this then e-mail me. Application procedures are described here.

Publications

Most of my publications (DBLP) are available on-line.

Research Group

Dr. Adam Bakewell, Research Fellow
Mohamed Menaa, Doctoral Student
Alex Smith, Doctoral Student
Zaid Al-Zobaidi, Doctoral Student

Tools

I was involved in the development of several game-based verification tools. Two of them are available for download:

Mage: the state of the art tool, which uses on-the fly model checking and approximation refinement;
GameChecker: an earlier tool which uses FDR as a back end. It supports unbounded integers.

Groups

I am a member of the local Verification, Principles of Programming and Modelling research Groups.

Grants

Epsrc EP/D070880/1: A Unified Approach to Compositional Software Modelling, Analysis and Verification (Advanced Fellowship)
Epsrc EP/E010180/1: The role of language covers in games-based abstraction and refinement (visiting grant for Mike Domaratzki)
Epsrc EP/D034906/1: Modular Abstraction and Abstraction Refinement: A Game-Semantic Approach (principal investigator)

Other research-related activities

Invited tutorial speaker LICS 2009
Program Committee member TLCA 2009, FOSSACS 2008, 2009, LICS 2010.
Co-chair of the Games for Logic and Programming Languages Workshop III @ Etaps 2008.
Guest editor of the special issue of APAL on game semantics.
PC member for the Games in Design and Verification Workshop @ CAV 2005.