IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2010 > Cartesian Abstraction and Verification of Multithreaded Programs

Alexander Malkis

Tuesday, June 1, 2010

11:00am Meeting room 302 (Mountain View), level 3

Alexander Malkis, Post-doctoral Researcher, IMDEA Software Institute

Cartesian Abstraction and Verification of Multithreaded Programs

Abstract:

We consider the refinement of a static analysis method called thread-modular verification. It was an open question whether such a refinement can be done automatically. We present a counterexample-guided abstraction refinement algorithm for thread-modular verification and demonstrate its potential, both theoretically and practically.