We use a declarative SMT-based approach to model-checking of infinite state systems to design a procedure for automatically estab- lishing the termination of backward reachability by using well-quasi-orderings. Besides showing that our procedure succeeds in many in-stances 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.
Automated termination in model checking modulo theories / A. Carioni, S. Ghilardi, S. Ranise - In: Reachability problems : 5th international workshop, RP 2011 Genoa, Italy, september 28-30, 2011 : proceedings / [a cura di] G. Delzanno, I. Potapov. - Berlin : Springer, 2011. - ISBN 9783642242878. - pp. 110-124 (( Intervento presentato al 5th. convegno International Workshop on Reachability Problems, RP 11 tenutosi a Genova, Italy nel 2011 [10.1007/978-3-642-24288-5_11].
Automated termination in model checking modulo theories
A. CarioniPrimo
;S. GhilardiSecondo
;
2011
Abstract
We use a declarative SMT-based approach to model-checking of infinite state systems to design a procedure for automatically estab- lishing the termination of backward reachability by using well-quasi-orderings. Besides showing that our procedure succeeds in many in-stances 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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
