Local Proofs for Linear-Time Properties of Concurrent Programs

This paper develops a local reasoning method to check for termination and other linear-time temporal properties of concurrent programs. In practice, it is often infeasible to model check over the full state space of a concurrent program. The method developed in this paper replaces such global reasoning with checks of (abstracted) individual processes. An automatic refinement step gradually exposes local state if necessary, ensuring that the method is complete. (I.e., a property is eventually either proved or disproved.) Experimental results show that local reasoning can hold a significant advantage over global reasoning.