Cartesian Abstraction and Verification of Multithreaded Programs

June 1, 2010

Alexander Malkis


Cartesian Abstraction and Verification of Multithreaded Programs

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

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.