dr. Gordon PACE
University of Malta
Malta
-----------------------------------
          
Model Checking Hardware Compilers (joint work with Koen Claessen)
-----------------------------------
          
ABSTRACT
-----------------------------------
The use of hardware compilers to generate complex circuits 
from a high-level description is becoming more and more prevalent 
in a variety of application areas. However, this introduces further 
risks as the compilation process may introduce errors in otherwise 
correct high-level descriptions  of circuits. In this talk, 
I will be presenting techniques to enable the automatic verification 
of hardware compilers through the use of finite-state model checkers 
and their application on a simple regular expression hardware compiler. 
It will be followed by a discussion on how these techniques can be 
further developed and used on more complex hardware-description languages.
          
SHORT CV
-----------------------------------
Dr. Gordon Pace is a lecturer in the Computer Science and AI department 
of the University of Malta. He was previously based in Chalmers University, 
Gothenburg in Sweden, INRIA-Rhone Alpes in France and 
Laboratoire Verimag also in France. His main research interests lie in 
formal methods for software and hardware design, embedded languages, 
synchronous languages and semantics of programming languages.

URL http://www.cs.um.edu.mt/gordon.pace