In this paper we introduce a technique to improve the efficiency of SAT calls in Bounded Model Checking (BMC) problems. The proposed technique is based on exploiting interpolation-based invariants as redundant constraints for BMC. Previous research addressed the issue using over-approximated state sets generated by BDD-based traversals. While a BDD engine could be considered as an external tool, interpolants are directly related to BMC problems, as they come from SAT-generated refutation proofs, so their role as a SAT-based earning is potentially higher. Our work aims at understanding whether and how interpolants could speed up BMC checks, as they represent constraints on forward and backward reachable states at given unrolling boundaries. Being this work preliminary, we do not address a tight integration between interpolant generation and exploitation. We thus clearly distinguish an interpolant generation (learning) phase and a subsequent interpolant exploitation phase in a BMC run. We experimentally evaluate costs, benefits, as well as invariant selection options, on a set of publicly available model checking problems.

Interpolation-based learning as a mean to speed-up Bounded Model Checking / Cabodi, Gianpiero; Camurati, Paolo Enrico; Palena, Marco; Pasini, Paolo; Vendraminetto, Danilo. - ELETTRONICO. - (2017). (Intervento presentato al convegno 15th International Conference on Software Engineering and Formal Methods tenutosi a Trento (Italy) nel September 4-8, 2017).

Interpolation-based learning as a mean to speed-up Bounded Model Checking

CABODI, Gianpiero;CAMURATI, Paolo Enrico;PALENA, MARCO;PASINI, PAOLO;VENDRAMINETTO, DANILO
2017

Abstract

In this paper we introduce a technique to improve the efficiency of SAT calls in Bounded Model Checking (BMC) problems. The proposed technique is based on exploiting interpolation-based invariants as redundant constraints for BMC. Previous research addressed the issue using over-approximated state sets generated by BDD-based traversals. While a BDD engine could be considered as an external tool, interpolants are directly related to BMC problems, as they come from SAT-generated refutation proofs, so their role as a SAT-based earning is potentially higher. Our work aims at understanding whether and how interpolants could speed up BMC checks, as they represent constraints on forward and backward reachable states at given unrolling boundaries. Being this work preliminary, we do not address a tight integration between interpolant generation and exploitation. We thus clearly distinguish an interpolant generation (learning) phase and a subsequent interpolant exploitation phase in a BMC run. We experimentally evaluate costs, benefits, as well as invariant selection options, on a set of publicly available model checking problems.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11583/2674458
 Attenzione

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