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
1999-03-28