Abstract
We present a tool that implements Owicki-Gries and rely-guarantee methods for the compositional verification of multi-threaded programs. Our tool computes the requisite auxiliary assertions automatically using an abstraction and refinement procedure. Our procedure is based on a Horn clause encoding of refinement queries and facilitates the discovery of thread-modular proofs when such proofs exist. We present the tool and its evaluation on a collection of benchmarks, including a direct comparison of the effectiveness of the proof rules. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Gupta, A., Popeea, C., & Rybalchenko, A. (2011). Threader: A constraint-based verifier for multi-threaded programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6806 LNCS, pp. 412–417). https://doi.org/10.1007/978-3-642-22110-1_32
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
