1997-1999: Post-doctoral research at SRI International (California, USA)

As a post-doctoral fellow (generously supported by a Lavoisier grant of the French Foreign Affairs Ministry and by a stipend from SRI) I have worked on two main topics. The first (with prof. Tom Henzinger at UC Berkeley) is a combined application of theorem proving and model checking for reachability analysis of hybrid systems  [HR98]. The second is an approach that combines the same ingredients plus abstraction, also for verifying safety properties but for (non-hybrid) infinite-state systems. The idea in the latter approach  [RS99] is to interactively discover abstractions and auxiliary invariants that are tailored to proving a given safety property. Indeed, it is rather common (in currently existing work on abstraction) to suppose that the abstraction function is ``known'', therefore to just concentrate on how to efficiently construct the abstract system and then model-check it. But finding the right abstraction is by itself a hard problem, as is finding auxiliary invariants in a deductive proof. Our approach assists the user in discovering these abstractions/invariants in a stepwise manner, by making at each step constructive use of failures in previous steps. I have also participated in the SAL (Symbolic Analysis Laboratory) project [BGL+00], a general framework for combining techniques and tools for the symbolic analysis of reactive systems.

Vlad Rusu