Electrical & Computer Engineering     |     Carnegie Mellon

Wednesday, August 7, 12:00-1:00 p.m. HH-1112

Oded Maler
Senior Researcher ("Directeur de Recherche"), CNRS

Combining Formal Verification and Timing Analysis of Digital Circuits

In 1995, together with Amir Pnueli, we have shown that the bi-bounded gate delay model can be translated rather elegantly into the timed automata of Alur and Dill. This implies that, in principle, verification tools based on timed automata can be used to extend formal verification from the "functional" to the "performance" domains. However, the path from "in principle" to "in practice" goes through the state and clock explosion problem, which is much more severe in timed automata than in untimed models. In this talk I will explain the model and the methodology and survey several heroic, but sporadic, attempts to verify certain classes of circuit using the tool Kronos, developed at Verimag and its derivatives (SMI, OpenKronos, and IF) including the most recent results based on approximation techniques which seem to be applicable to very large circuits. These techniques are the topic of a recent research project sponsored by Intel.
Oded Maler is a senior researcher ("Directeur de Recherche") at the CNRS (French national research council) and is located at the VERIMAG laboratory in Grenoble where he is responsible for the "timed and hybrid systems" group. He holds a B.A. degree from the Technion, Haifa in computer science, a M.Sc. from Tel-Aviv University in management science and a Ph.D. from Weizmann Institute, Rehovot, in computer science. His main research agenda is concerned with the exportation toward other domains - most notably control theory, scheduling and circuit timing analysis - of automata-theoretic analysis techniques used in verification.