Refinement of Thread-Modular Verification

  • Alexander Malkis | University of Freiburg, Germany

Thread-modular verification à la Flanagan and Qadeer is a promising approach for avoiding the state explosion during the verification of concurrent programs. The method is polynomial in the number of threads. It can be phrased as a program analysis with a fixed `Cartesian abstraction’. We propose a flexible refinement of this abstraction that allows one to adapt the
precision while preserving the polynomial complexity. Our
experimental results demonstrate the practical potential of the resulting method. This is joint work with Andrey Rybalchenko and Andreas Podelski.

Speaker Details

Since 2004, Alexander Malkis has been a PhD student under the supervision of Andreas Podelski, first at the Max Planck Institute in Saarbrücken, then at the University of Freiburg, Germany. His field of interests include program analysis and verification.http://swt.informatik.uni-freiburg.de/alexmalk

    • Portrait of Jeff Running

      Jeff Running

Watch Next