Compositional Termination Proofs for Multi-threaded Programs

Abstract. Automated verification of multi-threaded programs is difficult. Direct treatment of all possible thread interleavings by reasoning about the program globally is a prohibitively expensive task, even for small programs. Rely-guarantee reasoning is a promising technique to address this challenge by reducing the verification problem to reasoning about each thread individually with the help of assertions about other threads. In this paper, we propose a proof rule that uses rely-guarantee reasoning for compositional verification of termination properties. The crux of our proof rule lies in its compositionality wrt. the thread structure of the program and wrt. the applied termination arguments – transition invariants. We present a method for automating the proof rule using an ion refinement procedure that is based on solving recursion-free Horn clauses. To deal with termination, we extend an existing Hornclause solver with the capability to handle well-foundedness constraints....

• Type: Journal
• Year: 2012
• Where: TACAS
• Authors: Corneliu Popeea, Andrey Rybalchenko
• Keywords: Algorithms, Micro Benchmarks, Proof Rule, TACAS 2012, Transition Invariants