Department of Information Technology

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:

  1. the proof system by Owicki and Gries
  2. thread-modular model-checking by Flanagan and Qadeer
  3. 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.

Back to the seminar page

Updated  2009-11-25 10:54:15 by Frédéric Haziza.