This paper describes Split, a compositional verifier for safety and general Ltl properties of shared-variable, multi-threaded programs. The foundation is a computation of compact local invariants, one for each process, which are used for constructing a proof for the property. An automatic refinement procedure gradually exposes more local information, until a decisive result (proof/disproof) is obtained. © 2010 Springer-Verlag.
CITATION STYLE
Cohen, A., Namjoshi, K. S., & Sa’ar, Y. (2010). SPLIT: A compositional LTL verifier. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6174 LNCS, pp. 558–561). https://doi.org/10.1007/978-3-642-14295-6_47
Mendeley helps you to discover research relevant for your work.