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.