SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving

1. Abbott, J., Bigatti, A.M.: CoCoALib: a C++ library for computations in commutative algebra.. and beyond. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 73–76. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

2. Akbarpour, B., Paulson, L.C.: Metitarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning 44(3), 175–205 (2010)

   Article  MathSciNet  MATH  Google Scholar 

3. 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)

   Chapter  Google Scholar 

4. Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer (2010)

   Google Scholar 

5. Bauer, C., Frink, A., Kreckel, R.: Introduction to the GiNaC framework for symbolic computation within the C++ programming language. Journal of Symbolic Computation 33(1), 1–12 (2002)

   Article  MathSciNet  MATH  Google Scholar 

6. Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

7. Chauhan, P., Goyal, D., Hasteer, G., Mathur, A., Sharma, N.: Non-cycle-accurate sequential equivalence checking. In: Proc. of DAC 2009, pp. 460–465. ACM Press (2009)

   Google Scholar 

8. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)

   Chapter  Google Scholar 

9. Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. In: Proc. of SMT 2012. EPiC Series, vol. 20, pp. 88–97. EasyChair (2013)

   Google Scholar 

10. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

11. Corzilius, F., Ábrahám, E.: Virtual substitution for SMT-solving. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 360–371. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

12. Corzilius, F., Loup, U., Junges, S., Ábrahám, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442–448. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

13. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., Ábrahám, E.: PROPhESY: a PRObabilistic ParamEter SYthesis tool. In: Proc. of CAV 2015. LNCS, vol. 9207. Springer (2015)

    Google Scholar 

14. Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulas over ordered fields. Journal of Symbolic Computation 24, 209–231 (1995)

    Article  MATH  Google Scholar 

15. 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)

    Chapter  Google Scholar 

16. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

17. Fränzle, M., et al.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3–4), 209–236 (2007)

    MATH  Google Scholar 

18. Gao, S., Ganai, M.K., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: Proc. of FMCAD 2010, pp. 81–89. IEEE (2010)

    Google Scholar 

19. Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with \(\sf AProVE\). In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184–191. Springer, Heidelberg (2014)

    Google Scholar 

20. Granlund, T.: the GMP development team: GNU MP: The GNU Multiple Precision Arithmetic Library. http://gmplib.org

21. Haible, B., Kreckel, R.B.: CLN: Class Library for Numbers. http://www.ginac.de/CLN

22. Heintz, J., Roy, M.F., Solerno, P.: On the theoretical and practical complexity of the existential theory of reals. The Computer Journal 36(5), 427–431 (1993)

    Article  MathSciNet  MATH  Google Scholar 

23. Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Tech. Rep. 91–41, Research Institute for Symbolic Computation, Johannes Kepler University Linz (1991)

    Google Scholar 

24. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

25. Junges, S., Loup, U., Corzilius, F., Ábrahám, E.: On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers. In: Muntean, T., Poulakis, D., Rolland, R. (eds.) CAI 2013. LNCS, vol. 8080, pp. 186–198. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

26. Kremer, G., Corzilius, F., Junges, S., Schupp, S., Ábrahám, E.: CArL: Computer ARithmetic and Logic Library. https://github.com/smtrat/carl

27. Loup, U., Scheibler, K., Corzilius, F., Ábrahám, E., Becker, B.: A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 193–207. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

28. 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)

    Chapter  Google Scholar 

29. de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15–44. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

30. Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 485–501. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

31. Ravanbakhsh, H., Sankaranarayanan, S.: Counterexample guided synthesis of switched controllers for reach-while-stay properties. CoRR abs/1505.01180 (2015). http://arxiv.org/abs/1505.01180

32. Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. In: Proc. of MBMV 2013, pp. 231–241. Institut für Angewandte Mikroelektronik und Datentechnik, Fakultät für Informatik und Elektrotechnik, Universität Rostock (2013)

    Google Scholar 

33. Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation 3, 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

34. https://github.com/smtrat/smtrat/wiki

35. Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376–392. Springer (1998)

    Google Scholar 

36. Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1–2), 3–27 (1988)

    Article  MathSciNet  MATH  Google Scholar 

37. Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)

    Article  MathSciNet  MATH  Google Scholar 

38. Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references