zbMATH — the first resource for mathematics

Fairness modulo theory: a new approach to LTL software model checking. (English) Zbl 1381.68157
Kroening, Daniel (ed.) et al., Computer aided verification. 27th international conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015. Proceedings. Part I. Cham: Springer (ISBN 978-3-319-21689-8/pbk; 978-3-319-21690-4/ebook). Lecture Notes in Computer Science 9206, 49-66 (2015).
Summary: The construction of a proof for unsatisfiability is less costly than the construction of a ranking function. We present a new approach to LTL software model checking (i.e., to statically analyze a program and verify a temporal property from the full class of LTL including general liveness properties) which aims at exploiting this fact. The idea is to select finite prefixes of a path and check these for infeasibility before considering the full infinite path. We have implemented a tool which demonstrates the practical potential of the approach. In particular, the tool can verify several benchmark programs for a liveness property just with finite prefixes (and thus without the construction of a single ranking function).
For the entire collection see [Zbl 1342.68028].

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX Cite
Full Text: DOI