Misplaced Pages

This article may be too technical for most readers to understand. Please help improve it to make it understandable to non-experts, without removing the technical details. (November 2023) (Learn how and when to remove this message)

In computer science and mathematical logic, Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 (stylized cvc5); earlier versions include CVC, CVC Lite, and CVC3. Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats. cvc5 has bindings for C++, Python, and Java.

CVC4 competed in SMT-COMP in the years 2014-2020, and cvc5 has competed in the years 2021-2022. CVC4 competed in SyGuS-COMP in the years 2015-2019, and in CASC in 2013-2015.

CVC4 uses the DPLL(T) architecture, and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors, floating-point arithmetic, strings, (co)-datatypes, sequences (used to model dynamic arrays), finite sets and relations, separation logic, and uninterpreted functions among others. cvc5 additionally supports finite fields.

In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning, which is the problem of constructing a formula B that can be conjoined with a formula A to prove a goal formula C.

cvc5 has been subject to several independent test campaigns.

Applications

CVC4 has been applied to the synthesis of recursive programs. and to the verification of Amazon Web Services access policies. CVC4 and cvc5 have been integrated with Coq and Isabelle. CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.

References

1. "Release cvc5-1.0.8 · cvc5/cvc5". GitHub. Retrieved 2023-11-29.
2. Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo Theories", Handbook of Model Checking, Cham: Springer International Publishing, pp. 305–343, doi:10.1007/978-3-319-10575-8_11, ISBN 978-3-319-10575-8
3. Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022). "Flexible Proof Production in an Industrial-Strength SMT Solver". In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning. Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35. doi:10.1007/978-3-031-10769-6_3. ISBN 978-3-031-10769-6. S2CID 250164402.
4. (Barbosa et al. 2022, p. 417)
5. "Participants". SMT-COMP. Retrieved 2023-11-29.
6. "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.
7. • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and Analysis of SyGuS-Comp'15". Electronic Proceedings in Theoretical Computer Science. 202: 3–26. arXiv:1602.01170. doi:10.4204/EPTCS.202.3. ISSN 2075-2180. S2CID 2086015.
   • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 229: 178–202. arXiv:1611.07627. doi:10.4204/EPTCS.229.13. ISSN 2075-2180. S2CID 440389.
   • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 260: 97–115. arXiv:1711.11438. doi:10.4204/EPTCS.260.9. ISSN 2075-2180. S2CID 37464992.
8. Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9.
9. Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
10. Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "Invertibility Conditions for Floating-Point Formulas". In Dillig, Isil; Tasiran, Serdar (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 116–136. doi:10.1007/978-3-030-25543-5_8. ISBN 978-3-030-25543-5.
11. Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). "A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings". In Lutz, Carsten; Ranise, Silvio (eds.). Frontiers of Combining Systems. Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
12. Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "A Decision Procedure for (Co)datatypes in SMT Solvers". In Felty, Amy P.; Middeldorp, Aart (eds.). Automated Deduction - CADE-25. Lecture Notes in Computer Science. Vol. 9195. Cham: Springer International Publishing. pp. 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
13. Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences". Journal of Automated Reasoning. 67 (3): 32. doi:10.1007/s10817-023-09682-2. ISSN 1573-0670. S2CID 261829653.
14. Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT". In Olivetti, Nicola; Tiwari, Ashish (eds.). Automated Reasoning. Lecture Notes in Computer Science. Vol. 9706. Cham: Springer International Publishing. pp. 82–98. doi:10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1.
15. Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "Relational Constraint Solving in SMT". In de Moura, Leonardo (ed.). Automated Deduction – CADE 26. Lecture Notes in Computer Science. Vol. 10395. Cham: Springer International Publishing. pp. 148–165. doi:10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5.
16. Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT" (PDF). In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Vol. 9938. Cham: Springer International Publishing. pp. 244–261. doi:10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. S2CID 6753369.
17. Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfiability Modulo Finite Fields". In Enea, Constantin; Lal, Akash (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 13965. Cham: Springer Nature Switzerland. pp. 163–186. doi:10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. S2CID 257235627.
18. Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis". Automated Reasoning. Lecture Notes in Computer Science. Vol. 12166. pp. 141–160. doi:10.1007/978-3-030-51074-9_9. ISBN 978-3-030-51073-2. PMC 7324138.
19. (Barbosa et al. 2022, p. 426)
20. • Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "Finding and Understanding Incompleteness Bugs in SMT Solvers". Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE '22. New York, NY, USA: Association for Computing Machinery. pp. 1–10. doi:10.1145/3551349.3560435. ISBN 978-1-4503-9475-8. S2CID 255441416.
    • Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26). "Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 69–81. doi:10.1109/ICSE48619.2023.00018. ISBN 978-1-6654-5701-9. S2CID 259860528.
    • Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 13372. Cham: Springer International Publishing. pp. 92–106. doi:10.1007/978-3-031-13188-2_5. ISBN 978-3-031-13188-2. S2CID 251447764.
    • Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236. doi:10.1109/ICSE48619.2023.00187. ISBN 978-1-6654-5701-9. S2CID 259860926.
    • Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "SMT Solver Validation Empowered by Large Pre-Trained Language Models". 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 1288–1300. doi:10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID 265055537. Retrieved 2023-11-29.
    • Bringolf, Mauro (2021). Fuzz-testing SMT Solvers with Formula Weakening and Strengthening (Master Thesis thesis). ETH Zurich. doi:10.3929/ethz-b-000507582.
21. Berman, Shmuel (2021-10-17). "Programming-by-example by programming-by-example: Synthesis of looping programs". Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity. SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery. pp. 19–21. arXiv:2108.08724. doi:10.1145/3484271.3484977. ISBN 978-1-4503-9088-0. S2CID 237213485.
22. Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (October 2018). Semantic-based Automated Reasoning for AWS Access Policies using SMT. IEEE. pp. 1–9. doi:10.23919/FMCAD.2018.8602994. ISBN 978-0-9835678-8-2. S2CID 52237693.
23. Rungta, Neha (2022). "A Billion SMT Queries a Day (Invited Paper)". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 3–18. doi:10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1. S2CID 251447649.
24. • For CVC4: Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: A Plug-In for Integrating SMT Solvers into Coq" (PDF). In Majumdar, Rupak; Kunčak, Viktor (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 10427. Cham: Springer International Publishing. pp. 126–133. doi:10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. S2CID 206701576.
    • For cvc5: (Barbosa et al. 2022, p. 425)
    • For cvc5: Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03). "An Interactive SMT Tactic in Coq using Abductive Reasoning". EPiC Series in Computing. 94. EasyChair: 11–22. doi:10.29007/432m. S2CID 259070258.
25. Desharnais, Martin; Vukmirović, Petar; Blanchette, Jasmin; Wenzel, Makarius (2022). "Seventeen Provers Under the Hammer". DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. doi:10.4230/LIPIcs.ITP.2022.8. S2CID 251322787.
26. Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C Bounded Model Checker". In Ábrahám, Erika; Havelund, Klaus (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 8413. Berlin, Heidelberg: Springer. pp. 389–391. doi:10.1007/978-3-642-54862-8_26. ISBN 978-3-642-54862-8.

• Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "Cvc5: A Versatile and Industrial-Strength SMT Solver". In Fisman, Dana; Rosu, Grigore (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 13243. Cham: Springer International Publishing. pp. 415–442. doi:10.1007/978-3-030-99524-9_24. ISBN 978-3-030-99524-9. S2CID 247857361.
• Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). "CVC4". In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 171–177. doi:10.1007/978-3-642-22110-1_14. ISBN 978-3-642-22110-1.

• Free and open-source software
• Free software programmed in C++
• Satisfiability modulo theories solvers
• Software using the BSD license