Owicki-Gries, Thread-Modular Model-Checking, Cartesian Abstraction
- 👤 Speaker: Alexander Malkis
- 📅 Date & Time: Tuesday 20 October 2009, 13:00 - 14:00
- 📍 Venue: Computer Laboratory, William Gates Building, Room SS03
Abstract
We examine three different approaches to verification of multithreaded programs:- the Owicki-Gries annotation together with a proof rule system
- 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.
Speaker’s 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. Till the 20th of November, he is interning at MSRC . More information about the speaker can be found at http://swt.informatik.uni-freiburg.de/~alexmalk.
Series This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computer Laboratory Automated Reasoning Group Lunches
- Computer Laboratory, William Gates Building, Room SS03
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Martin's interesting talks
- School of Technology
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Alexander Malkis
Tuesday 20 October 2009, 13:00-14:00