We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract transitions without computing explicitly the abstract system and is incremental with respect to the addition of predicates. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike current SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available, and can moreover be inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.

IC3 Modulo Theories via Implicit Predicate Abstraction / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - 8413:(2014), pp. 46-61. (Intervento presentato al convegno Tools and Algorithms for the Construction and Analysis of Systems (TACAS) tenutosi a Grenoble nel 2014) [10.1007/978-3-642-54862-8_4].

IC3 Modulo Theories via Implicit Predicate Abstraction

A. Cimatti;A. Griggio;S. Mover;S. Tonetta
2014-01-01

Abstract

We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract transitions without computing explicitly the abstract system and is incremental with respect to the addition of predicates. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike current SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available, and can moreover be inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.
2014
TACAS
-
Cham, Switzerland
Springer
9783642548611
Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.
IC3 Modulo Theories via Implicit Predicate Abstraction / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - 8413:(2014), pp. 46-61. (Intervento presentato al convegno Tools and Algorithms for the Construction and Analysis of Systems (TACAS) tenutosi a Grenoble nel 2014) [10.1007/978-3-642-54862-8_4].
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/343009
 Attenzione

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

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