My main research interests are automated software verification, timing analysis of binary programs, control and verification of timed systems. My recent research focussed on static analysis of C programs, energy and mean-payoff timed games and worst-case execution time (WCET) estimation. I am with the Department of Computing at Macquarie University, Sydney, Australia.

Research Projects

• Automated software verification
• Automatic computation of worst-case execution time (WCET analysis)
• Formal modeling and analysis of timed systems

Software (Scala packages)

• Expect for Scala a Scala implementation for Expect
• ScalaSMT an abstraction over the SMTLIB standard for Satisfiability Modulo Theory (SMT) solvers

Publications

Some publications can be found here. My DBLP publications list. My Google scholar public profile.

Collaborators

Here are some nice people I work or have worked with:

• Karine Altisen, VERIMAG, Grenoble, France
• Béatrice Bérard, LIP6, Université Pierre et Marie Curie, France
• Sebastian Biallas, RWTH, Aachen, Germany
• Patricia Bouyer, LSV, ENS Cachan, France
• Thomas Chatain, LSV, ENS Cachan, France
• Alexandre David, Aalborg University, Denmark
• Jérémy Dubreil, Facebook
• Ansgar Fehnker, USP, Suva, Fiji
• Alain Finkel, LSV, ENS Cachan, France
• Emmanuel Fleury, LaBRI, Univ. Bordeaux 1, France
• Serge Haddad, LSV, ENS Cachan, France
• Thomas A. Henzinger, IST, Austria
• Frédéric Herbreteau, LaBRI, Bordeaux, France
• Ralf Huuck, NICTA/DATA61, Sydney, Australia
• Claude Jard, AtlanSTIC and LINA, Nantes, France
• François Laroussinie, LIAFA, Université Paris Diderot - Paris 7, France
• Kim Guldstrand Larsen, Aalborg University, Denmark
• Hervé Marchand, IRISA/INRIA, Rennes, France
• Nicolas Markey, LSV, ENS Cachan, France
• John Mullins, Ecole Polytechnique de Montréal, Canada
• Mads Olesen, Allborg University, Denmark
• Jean-François Raskin, Université Libre de Bruxelles, Belgium
• Pierre-Alain Reynier, LIF, Marseille, France
• Vlad Rusu, INRIA, Lille, France
• Mark Ryan, University of Birmingham, UK
• Matt Roberts, Macquarie University, Sydney, Australia
• Pierre-Yves Schobbens, Facultés Universitaires Notre Dame de la Paix, Namur, Belgium
• Tony Sloane, Macquarie University, Sydney, Australia
• Grégoire Sutre, LaBRI, Université de Bordeaux I, France
• Stavros Tripakis, Aalto University, Finland, and UC Berkeley, USA
• Ron van der Meyden, School of Computer Science and Engineering, UNSW Sydney, Australia
• Chenyi Zhang, Oracle, Brisbane, Australia.

Verification tools

• UPPAAL Model Checking of Timed Automata
• UPPAAL-TiGA Efficient Controller Synthesis for Timed Automata
• CMC Compositional Model-Checking for Timed and Hybrid Automata
• KRONOS Model-Checking for Timed Automata
• HyTech Reachability analysis for Hybrid Automata. Here is a tgz hytech-for-osX.tgz for compiling HyTech under Mac OS X (unofficial version). To use see the README-OSX in src directory.
• PHAver Polyhedral Hybrid Automaton Verifyer (and How to Install it for Mac OSX)
• SPIN Model-Checking for Communicating Systems
• GOANNA Static analysis tool for C/C++ source code
• Roméo A tool for Time Petri Nets analysis
• Tina TIme petri Net Analyzer
• TIMES Tool for Modeling and Implementation of Embedded Systems