This paper develops a local reasoning method to check linear-time 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 reasoning with checks of (abstracted) individual processes. An automatic refinement step gradually exposes local state if necessary, ensuring that the method is complete. Experiments show that local reasoning can hold a significant advantage over global reasoning. © 2008 Springer-Verlag.
CITATION STYLE
Cohen, A., & Namjoshi, K. S. (2008). Local proofs for linear-time properties of concurrent programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 149–161). https://doi.org/10.1007/978-3-540-70545-1_15
Mendeley helps you to discover research relevant for your work.