Modular strategic SMT solving with SMT-RAT

[1] J. Abbott, A. M. Bigatti, CoCoALib: A C++ library for computations in commutative algebra . . . and beyond. Proc. of ICMS’10 (2010), vol. 6327 of LNCS, Springer, pp. 73–76. ⇒7, 12Search in Google Scholar

[2] E. Ábrahám, J. Nalbach, G. Kremer, Embedding the virtual substitution method in the model constructing satisfiability calculus framework. Proc. of SC-square’17 (2017), vol. 1974 of CEUR Workshop Proceedings, CEUR-WS.org. ⇒16Search in Google Scholar

[3] A. Albarghouthi, A. Gurfinkel, O. Wei, M. Chechik, Abstract analysis of symbolic executions. Proc. of CAV’10 (2010), vol. 6174 of LNCS, Springer, pp. 495–510. ⇒12Search in Google Scholar

[4] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli, CVC4. Proc. of CAV’11 (2011), vol. 6806 of LNCS, Springer, pp. 171–177. ⇒9, 14Search in Google Scholar

[5] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). http://www.SMT-LIB.org, 2016. ⇒20Search in Google Scholar

[6] C. Bauer, A. Frink, R. Kreckel, Introduction to the GiNaC framework for symbolic computation within the C++ programming language, Journal of Symbolic Computation33, 1 (2002) 1–12. ⇒7, 1210.1006/jsco.2001.0494Search in Google Scholar

[7] T. Bouton, D. C. B. de Oliveira, D. Déharbe, P. Fontaine, veriT: An open, trustable and efficient SMT-solver, Proc. of CADE-22 (2009), vol. 5663 of LNCS, Springer, pp. 151–156. ⇒9, 1410.1007/978-3-642-02959-2_12Search in Google Scholar

[8] M. Bromberger, C. Weidenbach, Fast cube tests for LIA constraint solving. Proc. of IJCAR’16 (2016), Springer, pp. 116–132. ⇒1510.1007/978-3-319-40229-1_9Search in Google Scholar

[9] C. W. Brown, M. Košta, Constructing a single cell in cylindrical algebraic decomposition, Journal of Symbolic Computation70 (2015) 14–48. ⇒1710.1016/j.jsc.2014.09.024Search in Google Scholar

[10] B. Buchberger, Gröbner bases: Applications. in: The Concise Handbook of Algebra. Kluwer Academic Publishers, 2002, pp. 265–268. ⇒12Search in Google Scholar

[11] P.-S. Chen, Y.-S. Hwang, R. D.-C. Ju, J.-K. Lee, Interprocedural probabilistic pointer analysis, IEEE Trans. Parallel Distrib. Syst. 15, 10 (2004) 893–907. ⇒ 12Search in Google Scholar

[12] A. Cimatti, A. Griggio, B. Schaafsma, B., R. Sebastiani, The MathSAT5 SMT solver. Proc. of TACAS’13, vol. 7795 of LNCS. Springer, 2013, pp. 93–107. ⇒910.1007/978-3-642-36742-7_7Search in Google Scholar

[13] G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata Theory and Formal Languages (1975), vol. 33 of LNCS, Springer, pp. 134–183. ⇒11, 12Search in Google Scholar

[14] F. Corzilius, Virtual substitution in SMT solving, Diploma thesis, RWTH Aachen University, 2011. ⇒1410.1007/978-3-642-22953-4_31Search in Google Scholar

[15] F. Corzilius, Integrating Virtual Substitution into Strategic SMT Solving. PhD thesis, RWTH Aachen University, 2016. ⇒15Search in Google Scholar

[16] F. Corzilius, G. Kremer, S. Junges, S. Schupp, E. Ábrahám, SMT-RAT: An open source C++ toolbox for strategic and parallel SMT solving. Proc. of SAT’15 (2015), vol. 9340 of LNCS, Springer, pp. 360–368. ⇒6, 7, 9, 15, 2010.1007/978-3-319-24318-4_26Search in Google Scholar

[17] F. Corzilius, U. Loup, S. Junges, S., E. Ábrahám, SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox. Proc. of SAT’12 (2012), vol. 7317 of LNCS, Springer, pp. 442–448. ⇒6, 710.1007/978-3-642-31612-8_35Search in Google Scholar

[18] G. B. Dantzig, Linear programming and extensions. Princeton University Press, 1963. ⇒1010.7249/R366Search in Google Scholar

[19] M. Davis, H. Putnam, A computing procedure for quantification theory. Journal of the ACM7, 3 (1960) 201–215. ⇒810.1145/321033.321034Search in Google Scholar

[20] L. de Moura, N. Bjørner, Z3: An efficient SMT solver. Proc. of TACAS’08 (2008), vol. 4963 of LNCS, Springer, pp. 337–340. ⇒9, 1410.1007/978-3-540-78800-3_24Search in Google Scholar

[21] L. M. de Moura, D. Jovanovic, A model-constructing satisfiability calculus. Proc. of VMCAI’13 (2013), vol. 7737 of LNCS, Springer, pp. 1–12. ⇒9, 16Search in Google Scholar

[22] B. Dutertre, Yices 2.2. Proc. of CAV’14 (2014), vol. 8559 of LNCS, Springer, pp. 737–744. ⇒9, 14Search in Google Scholar

[23] B. Dutertre, L. M. de Moura, A fast linear-arithmetic solver for DPLL(T). Proc. of CAV’06 (2006), vol. 4144 of LNCS, Springer, pp. 81–94. ⇒15Search in Google Scholar

[24] N. Eén, N. Sörensson, An extensible SAT-solver. Proc. of SAT’03 (2004), vol. 2919 of LNCS, Springer, pp. 502–518. ⇒15Search in Google Scholar

[25] P. Fontaine, M. Ogawa, T. Sturm, T., X. T. Vu, Subtropical satisfiability. Proc. of FroCoS’17 (2017), Springer, pp. 189–206. ⇒11, 16Search in Google Scholar

[26] C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, H. Zankl, SAT solving for termination analysis with polynomial interpretations. Proc. of SAT’07 (2007), Springer, pp. 340–354. ⇒15Search in Google Scholar

[27] S. Gao, M. Ganai, F. Ivančić, A. Gupta, S. Sankaranarayanan, E. M. Clarke, Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. Proc. of FMCAD’10 (2010), IEEE, pp. 81–90. ⇒10Search in Google Scholar

[28] K. O. Geddes, S. R. Czapor, G. Labahn, Algorithms for Computer Algebra. Kluwer Academic Publishers, 1992. ⇒710.1007/b102438Search in Google Scholar

[29] J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, R. Thiemann, Proving termination of programs automatically with AProVE. Proc. of IJCAR’14 (2014), vol. 8562 of LNAI, Springer, pp. 184–191. ⇒910.1007/978-3-319-08587-6_13Search in Google Scholar

[30] M. Grobelna, SAT-modulo-theories solving for pseudo-Boolean constraints. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14, 15Search in Google Scholar

[31] R. Haehn, Using equational constraints in an incremental CAD projection. Master’s thesis, RWTH Aachen University, 2017. ⇒14Search in Google Scholar

[32] E. M. Hahn, H. Hermanns, B. Wachter, L. Zhang, PARAM: A model checker for parametric Markov models. Proc. of CAV’10 (2010), vol. 6174 of LNCS, Springer, pp. 660–664. ⇒12Search in Google Scholar

[33] W. Hentze, Infeasible subsets for nonlinear SMT. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14Search in Google Scholar

[34] S. Herbort, D. Ratz, Improving the efficiency of a nonlinear-system-solver using a componentwise Newton method. Tech. Rep. 2/1997, Inst. für Angewandte Mathematik, University of Karlsruhe, 1997. ⇒10Search in Google Scholar

[35] D. Jovanović, Solving nonlinear integer arithmetic with MCSAT. Proc. of VM-CAI’17 (2017), Springer, pp. 330–346. ⇒20Search in Google Scholar

[36] D. Jovanović, L. de Moura, Solving non-linear arithmetic. Proc. of IJCAR’12 (2012), vol. 7364 of LNAI, Springer, pp. 339–354. ⇒16Search in Google Scholar

[37] S. Junges, On Gröbner bases in SMT-compliant decision procedures. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14Search in Google Scholar

[38] S. Junges, U. Loup, F. Corzilius, E. Ábrahám, E. On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers. Proc. of CAI’13 (2013), vol. 8080 of LNCS, Springer, pp. 186–198. ⇒15Search in Google Scholar

[39] T. V. Khanh, X. Vu, M. Ogawa, raSAT: SMT for polynomial inequality. Proc. of SMT’14 (2014), p. 67. ⇒9Search in Google Scholar

[40] G. Kremer, Isolating real roots using adaptable-precision interval arithmetic. Master’s thesis, RWTH Aachen University, 2013. ⇒14Search in Google Scholar

[41] G. Kremer, F. Corzilius, E. Ábrahám, A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. Proc. of CASC’16 (2016), vol. 9890 of LNCS, Springer, pp. 315–335. ⇒11, 15, 20Search in Google Scholar

[42] A. Krüger, Bitvectors in SMT-RAT and their application to integer arithmetics. Master’s thesis, RWTH Aachen University, 2015. ⇒14, 15Search in Google Scholar

[43] J. P. Marques-Silva, K. A. Sakallah, Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers48 (1999) 506–521. ⇒8Search in Google Scholar

[44] J. Nalbach, Embedding the virtual substitution in the MCSAT framework. Bachelor’s Thesis, RWTH Aachen University, 2017. ⇒14Search in Google Scholar

[45] L. Netz, Using Horner schemes to improve the efficiency and precision of interval constraint propagation. Bachelor’s Thesis, RWTH Aachen University, 2015. ⇒ 14Search in Google Scholar

[46] L. Neuberger, Generation of infeasible subsets in less-lazy SMT-solving for the theory of uninterpreted functions. Bachelor’s Thesis, RWTH Aachen University, 2015. ⇒14Search in Google Scholar

[47] J. Redies, An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14Search in Google Scholar

[48] SMT-COMP 2017 result summary. http://smtcomp.sourceforge.net/2017/results-toc.shtml, 2017. ⇒21Search in Google Scholar

[49] S. Schupp, Interval constraint propagation in SMT compliant decision procedures. Master’s thesis, RWTH Aachen University, 2013. ⇒14, 15Search in Google Scholar

[50] D. Scully, Preprocessing for solving non-linear real-arithmetic formulas. Bachelor’s Thesis, RWTH Aachen University, 2012. ⇒14Search in Google Scholar

[51] G. S. Tseitin, On the complexity of derivation in propositional calculus. in: Automation of Reasoning. Springer, 1983, pp. 466–483. ⇒810.1007/978-3-642-81955-1_28Search in Google Scholar

[52] V. X. Tung, T. Van Khanh, M. Ogawa, raSAT: An SMT solver for polynomial constraints. Formal Methods in System Design51, 3 (2017), 462–499. ⇒14, 20Search in Google Scholar

[53] T. Viehmann, Projection operators for the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14Search in Google Scholar

[54] T. Viehmann, G. Kremer, E. Ábrahám, Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving. Proc. of SC-square’17 (2017), vol. 1974 of CEUR Workshop Proceedings, CEUR-WS.org. ⇒15Search in Google Scholar

[55] V. Weispfenning, Quantifier elimination for real algebra – the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8, 2 (1997), 85–101. ⇒10Search in Google Scholar

[56] T. Winkler, Using Thom’s lemma for real algebraic numbers in the CAD. Bachelor’s Thesis, RWTH Aachen University, 2016. ⇒14Search in Google Scholar