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.