Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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)
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)
Fuhrman, O., Hoory, S.: An Example of a Δ-extendible Proof with a Spurious Interpolant. Technical Report H-0265, IBM Haifa Research Lab (2009)
Gershman, R., Koifman, M., Strichman, O.: An approach for extracting a small unsatisfiable core. Form. Methods Syst. Des. 33(1-3), 1–27 (2008)
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)
Li, B., Wang, C., Somenzi, F.: A satisfiability-based approach to abstraction refinement in model checking. Electr. Notes Theor. Comput. Sci. 89(4) (2003)
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)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal ACM 32, 733–749 (1985)
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)
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)
Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115–125 (1968)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fuhrmann, O., Hoory, S. (2009). On Extending Bounded Proofs to Inductive Proofs. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)