Compositional verification of multi-threaded programs

We introduce a novel verification method for multi-threaded programs that is fully automated and enables scalable compositional reasoning in reference [2] below. To achieve full automation, our technique supports abstraction refinement, which we realize with another research contribution, a constraint solver for Horn clauses over linear arithmetic constraints. We extend this method from safety to termination properties in [5] and published a tool paper describing our implementation of these algorithms in the most prestigious verification conference [4]. We solve two additional challenges in handling abstraction of control-flow [1] and solving Horn clauses in the presence of uninterpreted functions [3].

  1. ATVA 2010 Non-monotonic refinement of control abstraction for concurrent programs (pdf) (slides)
  2. POPL 2011 Predicate abstraction and refinement for verifying multi-threaded programs (pdf)
  3. APLAS 2011 Solving recursion-free Horn clauses over LI+UIF (pdf) (pdf with proofs)
  4. CAV 2011 Threader: A constraint-based verifier for multi-threaded programs (pdf) (slides) (source code for slides) (project webpage)
  5. TACAS 2012 Compositional termination proofs for multi-threaded programs (pdf) (slides)

This project has been carried at the Technical University Munich and is joint work with Ashutosh Gupta and Andrey Rybalchenko.