Elamur Research⌕
☰
home / papers / 2022 / cvc5: A Versatile and Industrial-Strength SMT Solver

cvc5: A Versatile and Industrial-Strength SMT Solver

Paper · 2022 · Haniel Barbosa, Clark Barrett, Martin Brain et al.

Summary

The paper presents cvc5, the successor to CVC4 in the cooperating validity checker (CVC) family of SMT solvers. SMT solvers are back-end reasoning engines for verification, model checking, security, test generation and synthesis. cvc5 is not a rewrite. It extends the CVC4 code base and was renamed to reflect a largely new developer team and substantial changes to the tool. The authors describe its architecture: a CDCL(T) SMT Solver core built on a customized MiniSat, with Preprocessor, Rewriter, Propositional Engine and Theory Engine modules. Abduction, interpolation, SyGuS and quantifier elimination are layered on top of this core. Additions since CVC4 1.8 include:

  • a new C++ API with Python and Java bindings
  • a new bit-vector solver
  • proof production
  • a new non-linear arithmetic procedure
  • syntax-guided quantifier instantiation

On the full non-incremental SMT-LIB set, cvc5 solves the most benchmarks overall compared with CVC4 and Z3. It falls behind CVC4 in a few divisions. Together with its industrial adoption, these results support the claim that cvc5 is both versatile and suited to production use.

Key points

  • The evaluation covered 379,750 SMT-LIB benchmarks, run with a 20-minute limit, one CPU core and 8GB RAM per run. It excluded 45 + 1128 benchmarks that SMT-LIB misclassifies, and the solvers never disagreed on any result.
  • The Proof Module emits unsatisfiability proofs in three formats: Alethe, Lean 4 and LFSC. The CLI accepts SMT-LIBv2, SyGuS2 and TPTP as input.
  • The Preprocessor runs 34 passes in a fixed order. Theory combination uses the polite mechanism with care graphs.
  • cvc5 is weaker than CVC4 on QF LinearIntArith (due to proof-related refactoring), QF Equality+Bitvec and QF Strings.
  • Industrial users include Zelkova (AWS), Boogie/Dafny/Move Prover, Certora, Isabelle's Sledgehammer and SPARK. The solver is released under the 3-clause BSD license.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States567 works · 335,190 citations🎓Bar-Ilan UniversityRamat Gan · Israel150 works · 25,428 citations🎓Universidade Federal de Minas GeraisBelo Horizonte · Brazil5 works · 39,300 citations🎓City, University of LondonLondon · United Kingdom2 works · 763 citations

Also on the byline: University of Iowa.

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksSoftware · 150 works

🧭 Topics 2Research subjects and languages the work is about.Machine translation · 1,109 worksReasoning · 1,948 works

Cite

Cite as Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS 2022 (LNCS 13,243).

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{barbosa2022cvc5,
  title = {{cvc5: A Versatile and Industrial-Strength SMT Solver}},
  author = {Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar},
  booktitle = {TACAS 2022 (LNCS 13243)},
  year = {2022},
  doi = {10.1007/978-3-030-99524-9\_24},
  url = {https://doi.org/10.1007/978-3-030-99524-9_24}
}

References

90 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. 1. Ábrahám, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119, 100633 (2021). https://doi.org/10.1016/j.jlamp.2020.100633 2. Al… ↗
  2. IEEE (2013), — Syntax-Guided Synthesis https://ieeexplore.ieee.org/ document/6679385/ 3. Alur, R., Bodı́k, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, Oc… ↗
  3. IEEE (2013), http://ieeexplore.ieee.org/document/ 6679385/ 4. Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TAC… — [doi:10.1007/978-3-662-54577-5](https://doi.org/10.1007/978-3-662-54577-5) ↗
  4. Springer (2011). https://doi.org/10.1007/978-3-642-25379-9 12 6. cvc5 Authors: cvc5 developer documentation. https://github.com/cvc5/cvc5/wiki (2021) 7. cvc5 Authors: cvc5 SMT-COMP 2021 Single Query run script. https://github.com/cvc5/cvc5/blob/smtcomp2021/contrib/competitions/smt-comp/ run-script-… — [doi:10.1007/978-3-642-25379-9](https://doi.org/10.1007/978-3-642-25379-9) ↗
  5. Springer (2020). https://doi.org/10.1007/978-3-030-53288-8 9 11. Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K.S., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: Bjørner, N., Gurfinkel, A. (eds.) 2018 Formal Meth… — [doi:10.1007/978-3-030-53288-8](https://doi.org/10.1007/978-3-030-53288-8) ↗
  6. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8602994 12. Bansal, K.: A branching heuristic in cvc4 smt solver. https://kshitij.io/articles/ cvc4-branching-heuristic.pdf (2012) 13. Bansal, K., Barrett, C.W., Reynolds, A., Tinelli, C.: A new decision procedure for finite sets and cardinality const… — [doi:10.23919/fmcad.2018.8602994](https://doi.org/10.23919/fmcad.2018.8602994) ↗
  7. IEEE (2019). https://doi.org/10.23919/FMCAD.2019.8894267 18. Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 11716, pp. 35… — [doi:10.23919/fmcad.2019.8894267](https://doi.org/10.23919/fmcad.2019.8894267) ↗
  8. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6 3 19. Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and O… — [doi:10.1007/978-3-030-29436-6](https://doi.org/10.1007/978-3-030-29436-6) ↗
  9. Springer (2005). https://doi.org/10.1007/11804192 17 20. Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Components and Objects. pp. 364–387. — [doi:10.1007/11804192](https://doi.org/10.1007/11804192) ↗
  10. Springer (2005) 21. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 171–177. find
  11. Springer (2011) 22. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2020), http://smt-lib.org 23. Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the… ↗
  12. Springer-Verlag (Nov 2006), phnom Penh, Cambodia 24. Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1-2), 21–46 (2007). https://doi.org/10.3233/sat190028 25. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0.… — [doi:10.3233/sat190028](https://doi.org/10.3233/sat190028) ↗
  13. Springer (2004). https://doi.org/10.1007/978-3-540-27813-9 49 27. Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 298–302. — [doi:10.1007/978-3-540-27813-9](https://doi.org/10.1007/978-3-540-27813-9) ↗
  14. Springer (2007). https://doi.org/10.1007/978-3-540-73368-3 34 28. Beazley, D.M.: SWIG: an easy to use tool for integrating scripting languages with C and C++. In: Diekhans, M., Roseman, M. (eds.) Fourth Annual USENIX Tcl/Tk Workshop 1996, Monterey, California, USA, July 10-13, 1996. — [doi:10.1007/978-3-540-73368-3](https://doi.org/10.1007/978-3-540-73368-3) ↗
  15. USENIX Association (1996), https://www.usenix.org/legacy/publications/ library/proceedings/tcl96/beazley.html 29. Behnel, S., Bradshaw, R., Citro, C., Dalcin, L., Seljebotn, D.S., Smith, K.: Cython: The best of both worlds. Computing in Science & Engineering 13(2), 31–39 (2011) 30. Bertot, Y., Caste… ↗
  16. An EATCS Series, Springer (2004). https://doi.org/10.1007/978-3-662-07964-5 31. Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds… — [doi:10.1007/978-3-662-07964-5](https://doi.org/10.1007/978-3-662-07964-5) ↗
  17. Springer (2011). https://doi.org/10.1007/978-3-642-22438-6 11 33. Bouchet, M., Cook, B., Cutler, B., Druzkina, A., Gacek, A., Hadarean, L., Jhala, R., Marshall, B., Peebles, D., Rungta, N., Schlesinger, C., Stephens, C., Varming, C., Warfield, A.: Block public access: trust safety verification of ac… — [doi:10.1007/978-3-642-22438-6](https://doi.org/10.1007/978-3-642-22438-6) ↗
  18. ACM (2020). https://doi.org/10.1145/3368089.3409728 34. Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 5663, pp. 151–156. — [doi:10.1145/3368089.3409728](https://doi.org/10.1145/3368089.3409728) ↗
  19. Springer (2009). https://doi.org/10.1007/978-3-642-02959-2 12 35. Bouton, T., Oliveira, D.C.B.D., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient smt-solver. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Can… — [doi:10.1007/978-3-642-02959-2](https://doi.org/10.1007/978-3-642-02959-2) ↗
  20. Springer (2009). https://doi.org/10.1007/978-3-642-02959-2 12 36. Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C.W., Tinelli, C.: Invertibility conditions for floating-point formulas. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2… — [doi:10.1007/978-3-642-02959-2](https://doi.org/10.1007/978-3-642-02959-2) ↗
  21. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5 8 37. Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: TACAS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I. LNCS, vol. 11427, pp. 79–98. — [doi:10.1007/978-3-030-25543-5](https://doi.org/10.1007/978-3-030-25543-5) ↗
  22. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0 5 38. Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. pp… — [doi:10.1007/978-3-030-17462-0](https://doi.org/10.1007/978-3-030-17462-0) ↗
  23. IEEE (2009). https://doi.org/10.1109/FMCAD.2009.5351141 39. Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: IJCAR. Lecture Notes in Computer Science, vol. 9706, pp. 116–132. — [doi:10.1109/fmcad.2009.5351141](https://doi.org/10.1109/fmcad.2009.5351141) ↗
  24. Springer (2016) 40. Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Dieg… find
  25. USENIX Association (2008), http://www.usenix.org/ events/osdi08/tech/full papers/cadar/cadar.pdf 41. Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Ve… ↗
  26. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9 22 42. Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceed… — [doi:10.1007/978-3-319-08867-9](https://doi.org/10.1007/978-3-319-08867-9) ↗
  27. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6 29 43. Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: FroCos. Lecture Notes in Computer Science, vol. 9322, pp. 119–134. — [doi:10.1007/978-3-319-41540-6](https://doi.org/10.1007/978-3-319-41540-6) ↗
  28. Springer (2015) 44. Christ, J., Hoenicke, J., Nutz, A.: Smtinterpol: An interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7385, pp. 248–… find
  29. Springer (2012). https://doi.org/10.1007/978-3-642-31759-0 19 45. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and… — [doi:10.1007/978-3-642-31759-0](https://doi.org/10.1007/978-3-642-31759-0) ↗
  30. Springer (2013) 47. Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (JAIR) 40, 701–728 (2011). https://doi.org/10.1613/jair.3196 48. Cook, B.: Formal reasoning about the security of amazon web services. In: Chock… — [doi:10.1613/jair.3196](https://doi.org/10.1613/jair.3196) ↗
  31. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3 3 49. Corbett, R.: Gnu bison (2021), https://www.gnu.org/software/bison/ 50. Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver,… — [doi:10.1007/978-3-319-96145-3](https://doi.org/10.1007/978-3-319-96145-3) ↗
  32. Springer (2015). https://doi.org/10.1007/978-3-319-24318-4 26 51. Craig, W.: Linear reasoning. A new form of the herbrand-gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957). https://doi.org/10.2307/2963593 52. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-… — [doi:10.1007/978-3-319-24318-4](https://doi.org/10.1007/978-3-319-24318-4) ↗
  33. Springer (2012). https://doi.org/10.1007/978-3-642-33826-7 16 53. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005) 54. Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequali… — [doi:10.1007/978-3-642-33826-7](https://doi.org/10.1007/978-3-642-33826-7) ↗
  34. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9 49 56. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: CAV. Lecture Notes in Computer Science, vol. 4144, pp. 81–94. — [doi:10.1007/978-3-319-08867-9](https://doi.org/10.1007/978-3-319-08867-9) ↗
  35. Springer (2006) 57. Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT. Lecture Notes in Computer Science, vol. 2919, pp. 502–518. find
  36. Springer (2003) 58. Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: Smtcoq: A plug-in for integrating SMT solvers into coq. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 10427, pp. 126–133. find
  37. Springer (2017). https://doi.org/10.1007/978-3-319-63390-9 7 59. England, M., Bradford, R.J., Davenport, J.H., Wilson, D.J.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) Mathematical S… — [doi:10.1007/978-3-319-63390-9](https://doi.org/10.1007/978-3-319-63390-9) ↗
  38. Springer (2014). https://doi.org/10.1007/978-3-662-44199-2 68 60. Filliâtre, J., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Confere… — [doi:10.1007/978-3-662-44199-2](https://doi.org/10.1007/978-3-662-44199-2) ↗
  39. Springer (2013). https://doi.org/10.1007/978-3-642-37036-6 8 61. Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Note… — [doi:10.1007/978-3-642-37036-6](https://doi.org/10.1007/978-3-642-37036-6) ↗
  40. Springer (2007). https://doi.org/10.1007/978-3-540-73368-3 52 62. Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012). https://doi.org/10.1145/2093548.2093564 63. Griggio, A.: An Effective SMT Engine for Formal Verification. Ph.D. th… — [doi:10.1007/978-3-540-73368-3](https://doi.org/10.1007/978-3-540-73368-3) ↗
  41. ACM (2011). https://doi.org/10.1145/1993498.1993506 66. Hadarean, L.: An efficient and trustworthy theory solver for bit-vectors in satisfiability modulo theories. Ph.D. thesis, Citeseer (2015) 67. Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the th… — [doi:10.1145/1993498.1993506](https://doi.org/10.1145/1993498.1993506) ↗
  42. Springer (2015). https://doi.org/10.1007/978-3-662-48899-7 24 68. Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York… — [doi:10.1007/978-3-662-48899-7](https://doi.org/10.1007/978-3-662-48899-7) ↗
  43. Springer (2019). https://doi.org/10.1007/978-3-030-41600-3 11 69. Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association for Computing Machinery 40(1), 143–184 (Jan 1993) 70. Hauzar, D., Marché, C., Moy, Y.: Counterexamples from proof failures in SPARK. In… — [doi:10.1007/978-3-030-41600-3](https://doi.org/10.1007/978-3-030-41600-3) ↗
  44. Springer (2016). https://doi.org/10.1007/978-3-319-41591-8 15 71. Hughes, R.J.M.: Super combinators: a new implementation method for applicative languages. In: Symposium on LISP and Functional Programming. pp. 1–10 (1982) 72. Hyvärinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: An S… — [doi:10.1007/978-3-319-41591-8](https://doi.org/10.1007/978-3-319-41591-8) ↗
  45. Springer (2016). https://doi.org/10.1007/978-3-319-40970-2 35 73. Iosif, R., Serban, C., Reynolds, A., Sighireanu, M.: Encoding separation logic in smt-lib v2.5 (2018) 74. Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: LPAR (Yogyakarta). Lecture Notes in Computer Science, vol. 6397, pp… — [doi:10.1007/978-3-319-40970-2](https://doi.org/10.1007/978-3-319-40970-2) ↗
  46. Springer (2010) 75. Jovanovic, D., Barrett, C.W.: Being careful about theory combination. Formal Methods Syst. Des. 42(1), 67–90 (2013) 76. Jovanovic, D., Dutertre, B.: Libpoly: A library for reasoning about polynomials. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Worksh… find
  47. CEUR-WS.org (2017), http://ceur-ws.org/Vol-1889/paper3.pdf 77. Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for dpll(t)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6… ↗
  48. IEEE (2016). https://doi.org/10.1109/FMCAD.2016.7886666 78. King, T.: Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. Ph.D. thesis, New York University (2014) 79. King, T., Barrett, C.W., Dutertre, B.: Simplex with sum of infeasibiliti… — [doi:10.1109/fmcad.2016.7886666](https://doi.org/10.1109/fmcad.2016.7886666) ↗
  49. IEEE (2013), https://ieeexplore.ieee.org/document/6679409/ 80. King, T., Barrett, C.W., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. pp. 139–146. ↗
  50. IEEE (2014). https://doi.org/10.1109/FMCAD.2014.6987606 81. Leino, K.M.: Accessible software verification with dafny. IEEE Software 34(06), 94–97 (nov 2017). https://doi.org/10.1109/MS.2017.4121212 82. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M.,… — [doi:10.1109/fmcad.2014.6987606](https://doi.org/10.1109/fmcad.2014.6987606) ↗
  51. Springer (2010). https://doi.org/10.1007/978-3-642-17511-4 20 83. Liang, S.: The Java Native interface : programmer’s guide and specification / Sheng Liang. Java series, Addison-Wesley, Reading, Mass. ; Harlow, England (1999) 84. Liang, T., Reynolds, A., Tinelli, C., Barrett, C.W., Deters, M.: A DPL… — [doi:10.1007/978-3-642-17511-4](https://doi.org/10.1007/978-3-642-17511-4) ↗
  52. Springer (2014) 85. Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.W.: A decision procedure for regular membership and length constraints over unbounded strings. find
  53. In: FroCos. Lecture Notes in Computer Science, vol. 9322, pp. 135–150. Springer (2015) 86. Mattarei, C., Mann, M., Barrett, C.W., Daly, R.G., Huff, D., Hanrahan, P.: Cosa: Integrated verification for agile hardware design. In: Bjørner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided D… find
  54. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603014 87. Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, P… — [doi:10.23919/fmcad.2018.8603014](https://doi.org/10.23919/fmcad.2018.8603014) ↗
  55. Springer (2017). https://doi.org/10.1007/978-3-319-63046-5 10 88. de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021… — [doi:10.1007/978-3-319-63046-5](https://doi.org/10.1007/978-3-319-63046-5) ↗
  56. Springer (2021). https://doi.org/10.1007/978-3-030-79876-5 37 89. de Moura, L.M., Bjørner, N.: Efficient e-matching for SMT solvers. In: Pfen-ning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Lecture No… — [doi:10.1007/978-3-030-79876-5](https://doi.org/10.1007/978-3-030-79876-5) ↗
  57. Springer (2007). https://doi.org/10.1007/978-3-540-73595-3 13 90. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint… ↗
  58. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3 24, https://doi.org/10.1007/978-3-540-78800-3 24 91. de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD. pp. 45–52. — [doi:10.1007/978-3-540-78800-3](https://doi.org/10.1007/978-3-540-78800-3) ↗
  59. IEEE (2009) 92. Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621 (2020), https://arxiv.org/abs/2006.01621 93. Niemetz, A., Preiner, M.: Ternary propagation-based local search for more bit-precise reasoning. In: 2020 Formal Methods in Computer Aided Design, FM-CAD 2020, Ha… — [arXiv:2006.01621](https://arxiv.org/abs/2006.01621) ↗
  60. IEEE (2020). https://doi.org/10.34727/2020/isbn.978-3-85448-042-6 29 94. Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608–636 (2017). https://doi.org/10.1007/s10703-017-0295-6 95. Niemetz, A., Preiner, M., Reynolds, A… — [doi:10.34727/2020/isbn.978-3-85448-042-6](https://doi.org/10.34727/2020/isbn.978-3-85448-042-6) ↗
  61. Springer (2021). https://doi.org/10.1007/978-3-030-72013-18 97. Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C.W., Tinelli, C.: Towards bit-width-independent proofs in SMT solvers. In: Fontaine, P. (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduct… — [doi:10.1007/978-3-030-72013-18](https://doi.org/10.1007/978-3-030-72013-18) ↗
  62. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6 22 98. Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , btormc and boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification -30th International Conference, CAV 2018, Held as Part of the Federated Logic Conf… — [doi:10.1007/978-3-030-29436-6](https://doi.org/10.1007/978-3-030-29436-6) ↗
  63. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3 32 99. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll(T ). J. ACM 53(6), 937–977 (2006). https://doi.org/10.1145/1217856.1217859 100. Nipkow,… — [doi:10.1007/978-3-319-96145-3](https://doi.org/10.1007/978-3-319-96145-3) ↗
  64. Springer (2002). https://doi.org/10.1007/3-540-45949-9 101. Nötzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C.W., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2… — [doi:10.1007/3-540-45949-9](https://doi.org/10.1007/3-540-45949-9) ↗
  65. Springer (2019). https://doi.org/10.1007/978-3-030-24258-9 20 102. — [doi:10.1007/978-3-030-24258-9](https://doi.org/10.1007/978-3-030-24258-9) ↗
  66. Organizers, S.C.: SMT-COMP 2021. https://smt-comp.github.io/2021/ (2021) 103. ↗
  67. Organizers, S.C.: SyGuS-Comp 2019. https://sygus.org/comp/2019/ (2021) 104. Padhi, S., Polgreen, E., Raghothaman, M., Reynolds, A., Udupa, A.: The sygus language standard version 2.1 (2021) 105. Parr, T.: ANTLRv3 (2021), https://www.antlr3.org/ 106. Paxson, V.: Flex lexical analyser generator (2021)… ↗
  68. Springer (2008). https://doi.org/10.1007/978-3-540-78163-9 20 108. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: FroCoS. Lecture Notes in Computer Science, vol. 3717, pp. 48–64. — [doi:10.1007/978-3-540-78163-9](https://doi.org/10.1007/978-3-540-78163-9) ↗
  69. Springer (2005) 109. Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theor… find
  70. Springer (2018). https://doi.org/10.1007/978-3-319-89963-3 7 110. Reynolds, A., Barbosa, H., Larraz, D., Tinelli, C.: Scalable algorithms for abduction via enumerative syntax-guided synthesis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference,… — [doi:10.1007/978-3-319-89963-3](https://doi.org/10.1007/978-3-319-89963-3) ↗
  71. Springer (2020). https://doi.org/10.1007/978-3-030-51074-9 9 111. Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C.W., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, C… — [doi:10.1007/978-3-030-51074-9](https://doi.org/10.1007/978-3-030-51074-9) ↗
  72. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5 5 112. Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, Augus… — [doi:10.1007/978-3-030-25543-5](https://doi.org/10.1007/978-3-030-25543-5) ↗
  73. Springer (2015). https://doi.org/10.1007/978-3-319-21401-6 13 113. Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June… — [doi:10.1007/978-3-319-21401-6](https://doi.org/10.1007/978-3-319-21401-6) ↗
  74. Springer (2016). https://doi.org/10.1007/978-3-319-40229-1 10 114. Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conferen… — [doi:10.1007/978-3-319-40229-1](https://doi.org/10.1007/978-3-319-40229-1) ↗
  75. Springer (2015). https://doi.org/10.1007/978-3-319-21668-3 12 115. Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016,… — [doi:10.1007/978-3-319-21668-3](https://doi.org/10.1007/978-3-319-21668-3) ↗
  76. Springer (2015). https://doi.org/10.1007/978-3-662-46081-8 5 118. Reynolds, A., Nötzli, A., Barrett, C.W., Tinelli, C.: High-level abstractions for simplifying extended string constraints in SMT. In: CAV (2). Lecture Notes in Computer Science, vol. 11562, pp. 23–42. — [doi:10.1007/978-3-662-46081-8](https://doi.org/10.1007/978-3-662-46081-8) ↗
  77. Springer (2019) 119. Reynolds, A., Nötzli, A., Barrett, C.W., Tinelli, C.: A decision procedure for string to code point conversion. In: IJCAR (1). Lecture Notes in Computer Science, vol. 12166, pp. 218–237. find
  78. Springer (2020) 120. Reynolds, A., Nötzli, A., Barrett, C.W., Tinelli, C.: Reductions for strings and regular expressions revisited. In: FMCAD. pp. 225–235. find
  79. IEEE (2020) 121. Reynolds, A., Tinelli, C., Goel, A., Krstic, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8… find
  80. Springer (2013). https://doi.org/10.1007/978-3-642-39799-8 42 122. Reynolds, A., Tinelli, C., Goel, A., Krstic, S., Deters, M., Barrett, C.W.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) Automated Deduction - CADE-24 - 24th International Conference o… — [doi:10.1007/978-3-642-39799-8](https://doi.org/10.1007/978-3-642-39799-8) ↗
  81. Springer (2013). https://doi.org/10.1007/978-3-642-38574-2 26 123. Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C.W.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brası́lia, Brazil, Septem… — [doi:10.1007/978-3-642-38574-2](https://doi.org/10.1007/978-3-642-38574-2) ↗
  82. Springer (2017). https://doi.org/10.1007/978-3-319-66167-4 2 124. Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. pp. 195–202. — [doi:10.1007/978-3-319-66167-4](https://doi.org/10.1007/978-3-319-66167-4) ↗
  83. IEEE (2014). https://doi.org/10.1109/FMCAD.2014.6987613 125. Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part… — [doi:10.1109/fmcad.2014.6987613](https://doi.org/10.1109/fmcad.2014.6987613) ↗
  84. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6 39 126. Reynolds, A., Woo, M., Barrett, C.W., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: CAV (2). Lecture Notes in Computer Science, vol. 10427, pp. 453–474. — [doi:10.1007/978-3-319-94205-6](https://doi.org/10.1007/978-3-319-94205-6) ↗
  85. Springer (2017) 127. Schkufza, E., Sharma, R., Aiken, A.: Stochastic program optimization. Commun. ACM 59(2), 114–122 (2016). https://doi.org/10.1145/2863701 128. Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury… — [doi:10.1145/2863701](https://doi.org/10.1145/2863701) ↗
  86. Springer (2021). https://doi.org/10.1007/978-3-030-79876-5 26 130. Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conferenc… — [doi:10.1007/978-3-030-79876-5](https://doi.org/10.1007/978-3-030-79876-5) ↗
  87. Springer (2020). https://doi.org/10.1007/978-3-030-51074-9 14 131. Soos, M.: CryptoMiniSat. https://github.com/msoos/cryptominisat (2020) 132. Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification (CAV). Lecture N… — [doi:10.1007/978-3-030-51074-9](https://doi.org/10.1007/978-3-030-51074-9) ↗
  88. Springer (2002). https://doi.org/10.1007/3-540-45657-0 40 133. Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods in System Design 42(1), 91–118 (2013). https://doi.org/10.1007/s10703-012-0163-3 134. Sutcliffe, G.: The TPTP Proble… — [doi:10.1007/3-540-45657-0](https://doi.org/10.1007/3-540-45657-0) ↗
  89. Springer (2008). https://doi.org/10.1007/978-3-540-79124-9 10 136. Trentin, P.: Optimization Modulo Theories with OptiMathSAT. Ph.D. thesis, University of Trento (2019) 137. Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C.W., Dill, D.L.: The move p… — [doi:10.1007/978-3-540-79124-9](https://doi.org/10.1007/978-3-540-79124-9) ↗
  90. Springer (2020). https://doi.org/10.1007/978-3-030-53288-8 7 138. Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Nötzli, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Bit-Precise Reasoning via Int-Blasting, to appear in the proceedings of VMCAI 2022 — [doi:10.1007/978-3-030-53288-8](https://doi.org/10.1007/978-3-030-53288-8) ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/