Gordon Pace
Research
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.
(Postscript version)
(PDF version)
(BiBTeX entry)
- Formal Reasoning With Verilog HDL, with Jifeng He,
in Formal Techniques for Hardware and Hardware-Like Systems (FTH 98)
Maarstrand, Sweden, 1998.
(Postscript version)
(PDF version)
(Related Slides)
(BiBTeX entry)
- Correct Hardware Compilation With Verilog HDL,
Technical Report, 1999.
(Postscript version)
(PDF version)
(BiBTeX entry)
- The Semantics of Verilog Using Transition System Combinators,
in Formal Methods for Computer-Aided-Design (FMCAD 2000),
Austin, Texas, 2000 (in LNCS 1954).
(Postscript version)
(PDF version)
(Related Slides)
(BiBTeX entry)
- 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.
(Postscript version)
(PDF version)
(Related Slides)
(BiBTeX entry)
- An Embedded Language Framework for Hardware Compilation,
with Koen Claessen,
in Designing Correct Circuits 2002 (DCC 2002),
Grenoble, France, 2002.
(Postscript)
(PDF)
(Related Slides)
(BiBTeX entry)
- 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.
(Postscript)
(PDF)
(BiBTeX entry)
Some teaching I've done in the past
- Formal Languages and Automata, University of Malta, 1998-9.
(Notes)
(Labs)
- Formal Specification and Design using Z, University of Malta, 1998-9.
(Slides)
(Exercises)
- Language Hierarchies and Algorithmic Complexity, University of Malta, 1998-9.
(Notes)
- Hardware Description Languages: Verilog (as part of
Hardware
Description and Verification), Chalmers Technical University, Sweden, 2000.
(Slides)
- Hardware Description Languages for Synchronous Circuits (with
Koen Claessen),
Chalmers Technical University, Sweden, 2000.
(Course page)
(Slides)
Some Tools
- 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.
(Source code)
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.
(Homepage)
- I have done some work on the current version of
Lesar,
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)
convertor to
SMV input.
- Haslu: An experimental version of an embedding of
Lustre in
Haskell,
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.
(Source Code)
- 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
France
|
|