Model finding for recursive functions in SMT. (English) Zbl 1475.68448
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 133-151 (2016).
Summary: SMT solvers have recently been extended with techniques for finding models of universally quantified formulas in some restricted fragments of first-order logic. This paper introduces a translation that reduces axioms specifying a large class of recursive functions, including terminating functions, to universally quantified formulas for which these techniques are applicable. An evaluation confirms that the approach improves the performance of existing solvers on benchmarks from three sources. The translation is implemented as a preprocessor in the CVC4 solver and in a new higher-order model finder called Nunchaku.
For the entire collection see [Zbl 1337.68016].
For the entire collection see [Zbl 1337.68016].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
E-Darvin; SmallCheck; Nunchaku; Mace4; Sledgehammer; Kodkod; Leon; CVC4; QuickCheck; Darwin; SMT-LIB; z3; FINDER; Prover9; NitpickReferences:
| [1] | Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Morrisett, G., Uustalu, T. (eds.) ICFP 2013, pp. 197–208. ACM (2013) · Zbl 1323.68092 · doi:10.1145/2500365.2500597 |
| [2] | Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011) · doi:10.1007/978-3-642-22110-1_14 |
| [3] | Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard–Version 2.5. Technical report, The University of Iowa (2015). http://smt-lib.org/ |
| [4] | Baumgartner, P., Bax, J.: Proving infinite satisfiability. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 86–95. Springer, Heidelberg (2013) · Zbl 1406.68019 · doi:10.1007/978-3-642-45221-5_6 |
| [5] | Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58–74 (2009) · Zbl 1171.68040 · doi:10.1016/j.jal.2007.07.005 |
| [6] | Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system–Verification by translation to recursive functions. In: Scala 2013. ACM (2013) |
| [7] | Blanchette, J.C.: Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Softw. Qual. J. 21(1), 101–126 (2013) · doi:10.1007/s11219-011-9148-5 |
| [8] | Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109–128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5 |
| [9] | Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Autom. Reasoning 47(4), 369–398 (2011) · Zbl 1266.03021 · doi:10.1007/s10817-011-9234-1 |
| [10] | Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010) · Zbl 1291.68326 · doi:10.1007/978-3-642-14052-5_11 |
| [11] | Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Reppy, J. (ed.) ICFP 2015. ACM (2015) · Zbl 1360.68358 · doi:10.1145/2784731.2784732 |
| [12] | Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000, pp. 268–279. ACM (2000) · doi:10.1145/351240.351266 |
| [13] | Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 207–221. Springer, Heidelberg (2011) · Zbl 1341.03017 · doi:10.1007/978-3-642-22438-6_17 |
| [14] | Claessen, K., Sörensson, N.: New techniques that improve MACE-style model finding. In: MODEL (2003) |
| [15] | de Moura, L., Bjørner, N.S.: Efficient E-Matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007) · Zbl 1213.68578 · doi:10.1007/978-3-540-73595-3_13 |
| [16] | de Moura, L., Bjørner, N.: Relevancy propagation. Technical report, Microsoft Research, October 2007 |
| [17] | de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-78800-3_24 |
| [18] | Dunets, A., Schellhorn, G., Reif, W.: Automated flaw detection in algebraic specifications. J. Autom. Reasoning 45(4), 359–395 (2010) · Zbl 1207.68337 · doi:10.1007/s10817-010-9166-1 |
| [19] | Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009) · Zbl 1242.68280 · doi:10.1007/978-3-642-02658-4_25 |
| [20] | Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524 |
| [21] | Jackson, D.: Nitpick: a checkable specification language. In: FMSP 1996, pp. 60–69 (1996) |
| [22] | Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 291–306. Springer, Heidelberg (2010) · Zbl 1291.68352 · doi:10.1007/978-3-642-14052-5_21 |
| [23] | Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 214–228. Springer, Heidelberg (2013) · Zbl 1398.68484 · doi:10.1007/978-3-642-40885-4_15 |
| [24] | Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic. Ph.D. thesis, Technische Universität München (2009) |
| [25] | Kuncak, V., Jackson, D.: Relational analysis of algebraic datatypes. In: Wermelinger, M., Gall, H. (eds.) ESEC/FSE 2005. ACM (2005) · doi:10.1145/1095430.1081740 |
| [26] | Lindblad, F.: Property directed generation of first-order test data. In: Morazán, M. (ed.) TFP 2007, pp. 105–123. Intellect (2008) |
| [27] | McCune, W.: Prover9 and Mace4. http://www.cs.unm.edu/mccune/prover9/ |
| [28] | McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problems. Technical report, Argonne National Laboratory (1994) |
| [29] | Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 197–213. Springer, Heidelberg (2015) · Zbl 1465.68297 · doi:10.1007/978-3-319-21401-6_13 |
| [30] | Reynolds, A., Blanchette, J.C., Tinelli, C.: Model finding for recursive functions in SMT. In: Ganesh, V., Jovanović, D. (eds.) SMT 2015 (2015) · Zbl 1475.68448 |
| [31] | Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014, pp. 195–202. IEEE (2014) · doi:10.1109/FMCAD.2014.6987613 |
| [32] | Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013) · doi:10.1007/978-3-642-39799-8_42 |
| [33] | Reynolds, A., Tinelli, C., Goel, A., Krstić, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 377–391. Springer, Heidelberg (2013) · Zbl 1381.68275 · doi:10.1007/978-3-642-38574-2_26 |
| [34] | Reynolds, A.J.: Finite model finding in satisfiability modulo theories. Ph.D. thesis, The University of Iowa (2013) |
| [35] | Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. In: Gill, A. (ed.) Haskell 2008, pp. 37–48. ACM (2008) · doi:10.1145/1411286.1411292 |
| [36] | Slaney, J.K.: FINDER: finite domain enumerator system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798–801. Springer, Heidelberg (1994) · doi:10.1007/3-540-58156-1_63 |
| [37] | Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007) · Zbl 1186.68304 · doi:10.1007/978-3-540-71209-1_49 |
| [38] | Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1–13. Springer, Heidelberg (1995) · doi:10.1007/3-540-60675-0_35 |
| [39] | Weber, T.: SAT-based finite model generation for higher-order logic. Ph.D. thesis, Technische Universität München (2008) |
| [40] | Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Mellish, C.S. (ed.) IJCAI 1995, vol. 1, pp. 298–303. Morgan Kaufmann (1995) |
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.
