Owicki-Gries, Thread-Modular Model-Checking, Cartesian Abstraction

Add to your list(s) Download to your calendar using vCal

• Alexander Malkis
• Tuesday 20 October 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

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.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• 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
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.