On Extending Bounded Proofs to Inductive Proofs

  • Oded Fuhrmann
  • Shlomo Hoory
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


We propose a method for extending a bounded resolution proof to an unbounded inductive proof. More specifically, given a resolution proof that a state machine beginning at an initial state satisfies some property at cycle k, we show that the existence of a Δ-invariant cut implies that the property holds for cycles k + Δ, k + 2Δ, etc. We suggest a linear algorithm for identifying such Δ-extendible proofs and develop the required theory for covering all cycles by Δ-extendible proofs. To expose Δ-invariant cuts, we develop an efficient proof manipulation algorithm that rearranges the proof by the natural temporal order. We demonstrate the applicability of our techniques on a few real-life examples.


Formal verification resolution proofs extending proofs proof simplification 


  1. [BCCZ99]
    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDS. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. [BIFH+08]
    Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2008)Google Scholar
  3. [FH09]
    Fuhrman, O., Hoory, S.: An Example of a Δ-extendible Proof with a Spurious Interpolant. Technical Report H-0265, IBM Haifa Research Lab (2009)Google Scholar
  4. [GKS08]
    Gershman, R., Koifman, M., Strichman, O.: An approach for extracting a small unsatisfiable core. Form. Methods Syst. Des. 33(1-3), 1–27 (2008)CrossRefzbMATHGoogle Scholar
  5. [JM05]
    Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. [LWS03]
    Li, B., Wang, C., Somenzi, F.: A satisfiability-based approach to abstraction refinement in model checking. Electr. Notes Theor. Comput. Sci. 89(4) (2003)Google Scholar
  7. [McM03]
    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
  8. [SC85]
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal ACM 32, 733–749 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  9. [SK97]
    Stoffel, D., Kunz, W.: Record & play: a structural fixed point iteration for sequential circuit verification. In: ICCAD 1997: Proceedings of the 1997 IEEE/ACM international conference on Computer-Aided Design, Washington, DC, USA, pp. 394–399. IEEE Computer Society, Los Alamitos (1997)Google Scholar
  10. [SSS00]
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a sat-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. [Tse68]
    Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115–125 (1968)Google Scholar
  12. [ZM03a]
    Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. [ZM03b]
    Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE 2003: Proceedings of the conference on Design, Automation and Test in Europe, Washington, DC, USA, p. 10880. IEEE Computer Society, Los Alamitos (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Oded Fuhrmann
    • 1
  • Shlomo Hoory
    • 1
  1. 1.IBM Haifa Research LabIsrael

Personalised recommendations