My main research interests are formal methods for software and
hardware design, compositional verification, synchronous languages
and semantics of programming languages. I am
currently mainly working on compositional verification techniques for
model-checking asynchronous systems. I am also working on techniques for
combining synchronous languages in a safe, and efficient way.
Some papers to download
- Hardware Design Based on Verilog HDL, DPhil thesis,
Oxford University Computing Laboratory, 1998.
- Formal Reasoning With Verilog HDL, with Jifeng He,
in Formal Techniques for Hardware and Hardware-Like Systems (FTH 98)
Maarstrand, Sweden, 1998.
- Correct Hardware Compilation With Verilog HDL,
Technical Report, 1999.
- The Semantics of Verilog Using Transition System Combinators,
in Formal Methods for Computer-Aided-Design (FMCAD 2000),
Austin, Texas, 2000 (in LNCS 1954).
- Counter-Example Generation in Symbolic Abstract Model-Checking, with
Nicolas Halbwachs, and Pascal Raymond, in 6th International Workshop on
Formal Methods for Industrial Critical Systems (FMICS 2001),
Paris, France, 2001.
- An Embedded Language Framework for Hardware Compilation,
with Koen Claessen,
in Designing Correct Circuits 2002 (DCC 2002),
Grenoble, France, 2002.
- SPeeDI - A Verification Tool for Polygonal Hybrid Systems, with
Eugene Asarin, Gerardo Schneider and Sergio Yovine,
in Computer-Aided Verification (CAV 2002),
Copenhagen, Denmark, 2002.
Some teaching I've done in the past
- Formal Languages and Automata, University of Malta, 1998-9.
- Formal Specification and Design using Z, University of Malta, 1998-9.
- Language Hierarchies and Algorithmic Complexity, University of Malta, 1998-9.
- Hardware Description Languages: Verilog (as part of
Description and Verification), Chalmers Technical University, Sweden, 2000.
- Hardware Description Languages for Synchronous Circuits (with
Chalmers Technical University, Sweden, 2000.
- Simsem: A translator from Verilog to SMV
input, emulating the simulation semantics of the given program as described in my
FMCAD 2000 paper. It is written in Haskell.
Beware: This is full of bugs which I never intend to fix.
- Relic: Short for Regular Languages Interactive Classroom. It
was intended to be part of a bigger instruction toolkit Filfla, but which,
unfortunately, was never realised.
- I have done some work on the current version of
the model-checking tool for Lustre, to allow visualisation of
counter-examples under abstraction. The algorithm implemented is
described in the FMICS '01 paper. For the same toolset, I have also
written an EC (intermediate Lustre code)
- Haslu: An experimental version of an embedding of
very much in the spirit of Lava.
It runs using the Hugs interpreter. Please,
let me know if you're interested in this work, or are interested in using it.
- SPeeDI: Together with
Gerardo Schneider, I have implemented
a verification tool for Planar Differential Inclusions. A short tool presentation can
be found in the CAV 2002 paper. It will shortly be available for download.
INRIA Rhone-Alpes / VASY |
655, avenue de l'Europe
38330 Montbonnot St Martin