Improvements to the Implementation of Interpolant-Based Model Checking

  • João Marques-Silva
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


The evolution of SAT technology over the last decade has motivated its application in model checking, initially through the utilization of SAT in bounded model checking (BMC) and, more recently, in unbounded model checking (UMC). This paper addresses the utilization of interpolants in UMC and proposes two techniques for improving the original interpolant-based UMC algorithm. These techniques include improvements to the computation of interpolants, and redefining the organization of the unbounded model checking algorithm given the information extracted from interpolant computation.


  1. 1.
    Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic reachability analysis based on SAT solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 411. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Marques-Silva, J.: Optimizing the utilization of interpolants in SAT-based model checking. Technical Report RT-01-05, INESC-ID (January 2005)Google Scholar
  4. 4.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • João Marques-Silva
    • 1
  1. 1.IST/INESC-IDTechnical University of LisbonPortugal

Personalised recommendations