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.