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

Software (Scala packages)


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


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

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