Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 6405))
Included in the following conference series:
492Accesses
6Citations
Abstract
We present a proof-generating decision procedure for the quantifier-free fragment of first-order logic with the relations =, ≠, ≥, and > and argue that this logic, augmented with a set of theory-specific rewriting rules, is adequate for bit-level accurate verification. We describe our decision procedure from an algorithmic point of view and explain how it is possible to efficiently generate Craig interpolants for this logic.
Furthermore, we discuss the relevance of the logical fragment in software model checking and provide a preliminary evaluation of its applicability using an interpolation-based program analyser.
Supported by the Semiconductor Research Corporation (SRC) under contract no. 2006-TJ-1539 and by the EU FP7 STREP MOGENTES (project ID ICT-216679).
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
McMillan, K.L.: Applications of Craig interpolation to model checking. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 22–23. Springer, Heidelberg (2004)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62, 981–998 (1997)
McMillan, K.L.: An interpolating theorem prover. Theoretical Computer Science 345, 101–121 (2005)
Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground interpolation for the theory of equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 413–427. Springer, Heidelberg (2009)
Goel, A., Krstić, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 183–198. Springer, Heidelberg (2009)
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Cimatti, A., Sebastiani, R.: Building efficient decision procedures on top of SAT solvers. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 144–175. Springer, Heidelberg (2006)
Meir, O., Strichman, O.: Yet another decision procedure for equality logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 307–320. Springer, Heidelberg (2005)
Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Principles of Programming Languages, pp. 232–244. ACM, New York (2004)
Kroening, D., Weissenbacher, G.: Lifting Propositional Interpolants to the Word-Level. In: Formal Methods in Computer-Aided Design, pp. 85–89. IEEE, Los Alamitos (2007)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages, pp. 58–70. ACM, New York (2002)
Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant generation for UTVPI⋆. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 167–182. Springer, Heidelberg (2009)
Jain, H., Clarke, E.M., Grumberg, O.: Efficient craig interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 254–267. Springer, Heidelberg (2008)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 527–541. Springer, Heidelberg (2006)
Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Aspects of Computing (2009); (published Online FirstTM)
Author information
Authors and Affiliations
Computing Laboratory, Oxford University, UK
Daniel Kroening & Georg Weissenbacher
Computer Systems Institute, ETH Zurich, Switzerland
Georg Weissenbacher
- Daniel Kroening
Search author on:PubMed Google Scholar
- Georg Weissenbacher
Search author on:PubMed Google Scholar
Editor information
Editors and Affiliations
Bell Laboratories, Alcatel-Lucent, 600 Mountain Ave., 2B-435, 07974, Murray Hill, NJ, USA
Kedar Namjoshi
Saarland University, Campus E1, 66123, Saarbrücken, Germany
Andreas Zeller
IBM Research Laboratory, 31905, Haifa, Mount Carmel, Israel
Avi Ziv
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kroening, D., Weissenbacher, G. (2011). An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions. In: Namjoshi, K., Zeller, A., Ziv, A. (eds) Hardware and Software: Verification and Testing. HVC 2009. Lecture Notes in Computer Science, vol 6405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19237-1_15
Download citation
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-642-19236-4
Online ISBN:978-3-642-19237-1
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative