×

Automated termination in model checking modulo theories. (English) Zbl 1348.68124

Delzanno, Giorgio (ed.) et al., Reachability problems. 5th international workshop, RP 2011, Genoa, Italy, September 28–30, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24287-8/pbk). Lecture Notes in Computer Science 6945, 110-124 (2011).
Summary: We use a declarative SMT-based approach to model-checking of infinite state systems to design a procedure for automatically establishing the termination of backward reachability by using well-quasi-orderings. Besides showing that our procedure succeeds in many instances of problems covered by general termination results, we argue that it could predict termination also on single problems outside the scope of applicability of such general results.
For the entire collection see [Zbl 1223.68005].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

SMT-LIB
PDFBibTeX XMLCite
Full Text: DOI