
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.