We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic. © 2013 World Scientific Publishing Company.

Automated termination in model-checking modulo theories / Carioni, A.; Ghilardi, S.; Ranise, S.. - In: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE. - ISSN 0129-0541. - 24:2(2013), pp. 211-232. [10.1142/S012905411340008X]

Automated termination in model-checking modulo theories

Ranise S.
2013-01-01

Abstract

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic. © 2013 World Scientific Publishing Company.
2013
2
Carioni, A.; Ghilardi, S.; Ranise, S.
Automated termination in model-checking modulo theories / Carioni, A.; Ghilardi, S.; Ranise, S.. - In: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE. - ISSN 0129-0541. - 24:2(2013), pp. 211-232. [10.1142/S012905411340008X]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333272
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact