Local Proofs for Linear-Time Properties of Concurrent Programs

Abstract. This paper develops a local reasoning method to check lineartime temporal properties of concurrent programs. In practice, it is often infeasible to model check over the product state space of a concurrent program. The method developed in this paper replaces such global reaith checks of (abstracted) individual processes. An automatic refinement step gradually exposes local state if necessary, ensuring that the method is complete. Experiments with a prototype implementation show that local reasoning can hold a significant advantage over global reasoning.

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Ariel Cohen 0002, Kedar S. Namjoshi
• Keywords: CAV 2008, Concurrent Program, Hardware, Local Reasoning, Local Reasoning Method