Web VERIMAG
VERIMAG

Susanne Graf

Susanne.Graf@imag.fr       
Tel: (+33) 4 57 42 22 19     
Office 283 in IMAG building
Photo

 

NEWS

I am honored to have been awarded (along with Hassen Saidi) the 2022 CAV award for our ``pioneering work on predicate abstraction'' which was presented at CAV'97 in the paper “Construction of abstract state graphs with PVS” which proposed a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover (indeed, there was no SMT solver in those days). Predicate Abstraction had an important and lasting impact on the field of formal verification. It is indeed as relevant today as it was 25 years ago.

Design and Verification of Complex Embedded Systems

  • Design and Contract framework for Real-Time Embedded Systems (in the project with Wang Yi and the Embedded Systems group in Uppsala: ``UPDATE: Designed for Update of Next-Generation Embedded Systems'' (Knut&Alice Wallenberg Foundation))
  • Contract-based design and analysis of mixed critical systems
  • Design and Synthesis of Distributed Implementations form Global Specifications
  • Design-by-contract approaches
  • Component based design and verification (see also OMEGA and ARTIST)
  • Verification in the Large: IF language and Tool-set
  • Semantics of real-time and distributed systems,
  • Verification of infinite state systems by means of abstract interpretation (an overview)
  • Combination of abstraction, algorithmic model checking and theorem proving (Invariant Checker)
  • Temporal Logics and associated Verification Techniques