An interpolating theorem prover. (English) Zbl 1079.68092
Summary: We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem prover based on this method. The prover has been used for predicate refinement in the BLAST software model checker, and can also be used directly for model checking infinite-state systems, using interpolation-based image approximation.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
| 03C40 | Interpolation, preservation, definability |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J., Symbolic model checking: \(10^{20}\) states and beyond, (Proc. Fifth Annu. IEEE Symp. on Logic in Computer Science (1990), IEEE Computer Society Press: IEEE Computer Society Press Washington, DC), 1-33 · Zbl 0753.68066 |
| [2] | Craig, W., Three uses of the herbrand-gentzen theorem in relating model theory and proof theory, J. Symbolic Logic, 22, 3, 269-285 (1957) · Zbl 0079.24502 |
| [3] | L. de Moura, H. Rueß, M. Sorea, Lazy theorem proving for bounded model checking over infinite domains, in: 18th Conf. on Automated Deduction, CADE 2002, Lecture Notes in Computer Science, Springer, Copenhagen, Denmark, July 27-30, 2002.; L. de Moura, H. Rueß, M. Sorea, Lazy theorem proving for bounded model checking over infinite domains, in: 18th Conf. on Automated Deduction, CADE 2002, Lecture Notes in Computer Science, Springer, Copenhagen, Denmark, July 27-30, 2002. · Zbl 1072.68602 |
| [4] | T.A. Henzinger, R. Jhala, R. Majumdar, K.L. McMillan, Abstractions from proofs, in: ACM Symp. on Principles of Programming Language, POPL 2004, 2004, pp. 232-244.; T.A. Henzinger, R. Jhala, R. Majumdar, K.L. McMillan, Abstractions from proofs, in: ACM Symp. on Principles of Programming Language, POPL 2004, 2004, pp. 232-244. · Zbl 1325.68147 |
| [5] | Krajíc˘ek, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic, 62, 2, 457-486 (1997) · Zbl 0891.03029 |
| [6] | S.K. Lahiri, R.E. Bryant, B. Cook, A symbolic approach to predicate abstraction, in: Computer-Aided Verification, CAV 2003, 2003, pp. 141-153.; S.K. Lahiri, R.E. Bryant, B. Cook, A symbolic approach to predicate abstraction, in: Computer-Aided Verification, CAV 2003, 2003, pp. 141-153. · Zbl 1278.68181 |
| [7] | K.L. McMillan, Interpolation and sat-based model checking, in: Computer-Aided Verification, CAV 2003, 2003, pp. 1-13.; K.L. McMillan, Interpolation and sat-based model checking, in: Computer-Aided Verification, CAV 2003, 2003, pp. 1-13. · Zbl 1278.68184 |
| [8] | K.L. McMillan, N. Amla, Automatic abstraction without counterexamples, in: Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, 2003, pp. 2-17.; K.L. McMillan, N. Amla, Automatic abstraction without counterexamples, in: Internat. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, 2003, pp. 2-17. · Zbl 1031.68520 |
| [9] | M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient SAT solver, in: Design Automation Conference, 2001, pp. 530-535.; M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient SAT solver, in: Design Automation Conference, 2001, pp. 530-535. |
| [10] | Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Progr. Language Systems, 1, 2, 245-257 (1979) · Zbl 0452.68013 |
| [11] | Plaisted, D.; Greenbaum, S., A structure preserving clause form translation, J. Symbolic Comput., 2, 293-304 (1986) · Zbl 0636.68119 |
| [12] | Pudlák, P., Lower bounds for resolution and cutting plane proofs and monotone computations, J. Symbolic Logic, 62, 2, 981-998 (1997) · Zbl 0945.03086 |
| [13] | Saïdi, H.; Graf, S., Construction of abstract state graphs with PVS, (Grumberg, O., Computer-Aided Verification, CAV ’97, Vol. 1254 (1997), Springer: Springer Haifa, Israel), 72-83 |
| [14] | J.P.M. Silva, K.A. Sakallah, GRASP—a new search algorithm for satisfiability, in: Proc. Internat. Conf. on Computer-Aided Design, November 1996.; J.P.M. Silva, K.A. Sakallah, GRASP—a new search algorithm for satisfiability, in: Proc. Internat. Conf. on Computer-Aided Design, November 1996. · Zbl 1392.68388 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
