Abstract
In this paper (This is a short paper accepted in the new ideas and work-in-progress section of SEFM 2017.) 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 learning 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.
Similar content being viewed by others
Notes
- 1.
For sake of simplicity we refer here to the so called exact bound BMC problem, that look for counteraxamples of an exact length. Other forms of BMC problems exists, checking for lengths \(\le k\).
References
Biere, A., Jussila, T.: The Model Checking Competition Web Page. http://fmv.jku.at/hwmcc
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). doi:10.1007/3-540-49059-0_14
Cabodi, G., Nocco, S., Quer, S.: Improving SAT-based bounded model checking by means of BDD-based approximate traversals. J. Universal Comput. Sci. (JUCS) (2004). Special issue on SAT for Formal Verification and Testing
Cabodi, G., Palena, M., Pasini, P.: Interpolation with guided refinement: revisiting incrementality in sat-based unbounded model checking, pp. 43–50. FMCAD 2014 (2014)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_1
Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: 2009 Formal Methods in Computer-Aided Design, pp. 1–8, November 2009
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cabodi, G., Camurati, P., Palena, M., Pasini, P., Vendraminetto, D. (2017). Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper). In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-66197-1_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66196-4
Online ISBN: 978-3-319-66197-1
eBook Packages: Computer ScienceComputer Science (R0)