Owicki-Gries, thread-modular model checking and Cartesian abstraction
- Speaker
-
Alexander Malkis
, University of Freiburg-
-
- Bio
- Alexander Malkis has obtained his diploma from Saarbrücken, Germany, for a work on combinatorics of polyedges. At MPII and in Freiburg he was working on verification of multithreaded programs under the supervision of Prof. Dr. Andreas Podelski.
-
-
-
- Date and Time
Thursday, December 3rd, 2009 at 13.30
- Location
Polacksbaken, room 1146
- Abstract
-
We examine three different approaches to verification of multithreaded programs:
- the proof system by Owicki and Gries
- thread-modular model-checking by Flanagan and Qadeer
- abstract interpretation with a form of Cartesian abstraction, described by the speaker.
We show that all three methods have the same precision. We examine a way to increase the precision, up to completeness, which does not require auxiliary variables. We show polynomial time of the refined method on a practically interested program class.