Abstract
This paper describes the Vinter tool for extracting interpolants from proofs and minimising such interpolants using various measures. Vinter takes an input problem written in either SMT-LIB or TPTP syntax, generates so called local proofs and then uses a technique of playing in the grey areas of proofs to find interpolants minimal with respect to various measures. Proofs are found using either Z3 or Vampire, solving pseudo-boolean optimisation is delegated to Yices, while localising proofs and generating minimal interpolants is done by Vampire. We describe the use of Vinter and give experimental results on problems from bounded model checking.
We acknowledge funding from the University of Manchester and an EPSRC grant (Hoder and Voronkov), the FWF Hertha Firnberg Research grant T425-N23, the FWF National Research Network RiSE S11410-N23 and S11403-N23, the WWTF PROSEED grant ICT C-050 and the CeTAT project (Holzer and Kovács).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), www.SMT-LIB.org
Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)
Craig, W.: Three uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. Journal of Symbolic Logic 22(3), 269–285 (1957)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Hoder, K., Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 188–195. Springer, Heidelberg (2010)
Hoder, K., Kovacs, L., Voronkov, A.: Playing in the Grey Area of Proofs. In: Proc. of POPL, pp. 259–272 (2012)
Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)
Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 199–213. Springer, Heidelberg (2009)
McMillan, K.L.: An Interpolating Theorem Prover. Theor. Comput. Sci. 345(1), 101–121 (2005)
McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008)
McMillan, K.L.: Interpolants from Z3 Proofs. In: Proc. of FMCAD, pp. 19–27 (2011)
Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoder, K., Holzer, A., Kovács, L., Voronkov, A. (2012). Vinter: A Vampire-Based Tool for Interpolation. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)