Software:Cooperating Validity Checker
From HandWiki
Short description: SMT solver
| Developer(s) | Stanford University and University of Iowa |
|---|---|
| Initial release | 2022 |
| Stable release | 1.0.8[1]
/ 31 August 2023 |
| Written in | C++ |
| Operating system | Windows, Linux, macOS |
| Type | Theorem prover |
| License | BSD 3-clause |
| Website | cvc5 |
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.[2] 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.[3][4] cvc5 has bindings for C++, Python, and Java.
CVC4 competed in SMT-COMP in the years 2014-2020,[5] and cvc5 has competed in the years 2021-2022.[6] CVC4 competed in SyGuS-COMP in the years 2015-2019,[7] and in CASC in 2013-2015.
CVC4 uses the DPLL(T) architecture,[8] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,[9] floating-point arithmetic,[10] strings,[11] (co)-datatypes,[12] sequences (used to model dynamic arrays),[13] finite sets and relations,[14][15] separation logic,[16] and uninterpreted functions among others. cvc5 additionally supports finite fields.[17]
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.[18][19]
cvc5 has been subject to several independent test campaigns.[20]
Applications
CVC4 has been applied to the synthesis of recursive programs.[21] and to the verification of Amazon Web Services access policies.[22][23] CVC4 and cvc5 have been integrated with Coq[24] and Isabelle.[25] CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.[26]
References
- ↑ "Release cvc5-1.0.8 · cvc5/cvc5" (in en). https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.8.
- ↑ Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut et al., eds., "Satisfiability Modulo Theories" (in en), 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, https://doi.org/10.1007/978-3-319-10575-8_11, retrieved 2023-11-29
- ↑ Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias et al. (2022). "Flexible Proof Production in an Industrial-Strength SMT Solver". in Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (in en). Automated Reasoning. Lecture Notes in Computer Science. 13385. Cham: Springer International Publishing. pp. 15–35. doi:10.1007/978-3-031-10769-6_3. ISBN 978-3-031-10769-6. https://link.springer.com/chapter/10.1007/978-3-031-10769-6_3.
- ↑ (Barbosa Barrett)
- ↑ "Participants" (in en-US). https://smt-comp.github.io/2014/participants.html.
- ↑ "SMT-COMP" (in en-US). https://smt-comp.github.io/2022/participants.html.
- ↑
- 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. doi:10.4204/EPTCS.202.3. ISSN 2075-2180.
- 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. doi:10.4204/EPTCS.229.13. ISSN 2075-2180.
- 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. doi:10.4204/EPTCS.260.9. ISSN 2075-2180.
- ↑ 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 (in en). Computer Aided Verification. Lecture Notes in Computer Science. 8559. Cham: Springer International Publishing. pp. 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9. https://link.springer.com/chapter/10.1007/978-3-319-08867-9_43.
- ↑ 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 (in en). Computer Aided Verification. Lecture Notes in Computer Science. 8559. Cham: Springer International Publishing. pp. 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9. https://link.springer.com/chapter/10.1007/978-3-319-08867-9_45.
- ↑ Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). Dillig, Isil; Tasiran, Serdar. eds. "Invertibility Conditions for Floating-Point Formulas" (in en). Computer Aided Verification. Lecture Notes in Computer Science (Cham: Springer International Publishing): 116–136. doi:10.1007/978-3-030-25543-5_8. ISBN 978-3-030-25543-5. https://link.springer.com/chapter/10.1007/978-3-030-25543-5_8.
- ↑ 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 (in en). Frontiers of Combining Systems. Lecture Notes in Computer Science. 9322. Cham: Springer International Publishing. pp. 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0. https://link.springer.com/chapter/10.1007/978-3-319-24246-0_9.
- ↑ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "A Decision Procedure for (Co)datatypes in SMT Solvers". in Felty, Amy P.; Middeldorp, Aart (in en). Automated Deduction - CADE-25. Lecture Notes in Computer Science. 9195. Cham: Springer International Publishing. pp. 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6. https://link.springer.com/chapter/10.1007/978-3-319-21401-6_13.
- ↑ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz et al. (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences" (in en). Journal of Automated Reasoning 67 (3): 32. doi:10.1007/s10817-023-09682-2. ISSN 1573-0670. https://doi.org/10.1007/s10817-023-09682-2.
- ↑ 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 (in en). Automated Reasoning. Lecture Notes in Computer Science. 9706. Cham: Springer International Publishing. pp. 82–98. doi:10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1. https://link.springer.com/chapter/10.1007/978-3-319-40229-1_7.
- ↑ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "Relational Constraint Solving in SMT". in de Moura, Leonardo (in en). Automated Deduction – CADE 26. Lecture Notes in Computer Science. 10395. Cham: Springer International Publishing. pp. 148–165. doi:10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5. https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10.
- ↑ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT". in Artho, Cyrille; Legay, Axel; Peled, Doron (in en). Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. 9938. Cham: Springer International Publishing. pp. 244–261. doi:10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. https://hal.archives-ouvertes.fr/hal-01418883/file/Atva2016-2.pdf.
- ↑ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfiability Modulo Finite Fields". in Enea, Constantin; Lal, Akash (in en). Computer Aided Verification. Lecture Notes in Computer Science. 13965. Cham: Springer Nature Switzerland. pp. 163–186. doi:10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8.
- ↑ 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. 12166. pp. 141–160. doi:10.1007/978-3-030-51074-9_9. ISBN 978-3-030-51073-2.
- ↑ (Barbosa Barrett)
- ↑
- 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. https://doi.org/10.1145/3551349.3560435.
- 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. https://doi.org/10.1109/ICSE48619.2023.00018.
- Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers". in Shoham, Sharon; Vizel, Yakir (in en). Computer Aided Verification. Lecture Notes in Computer Science. 13372. Cham: Springer International Publishing. pp. 92–106. doi:10.1007/978-3-031-13188-2_5. ISBN 978-3-031-13188-2. https://link.springer.com/chapter/10.1007/978-3-031-13188-2_5.
- 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. https://doi.org/10.1109/ICSE48619.2023.00187.
- "SMT Solver Validation Empowered by Large Pre-Trained Language Models | IEEE Conference Publication | IEEE Xplore". doi:10.1109/ase56229.2023.00180. https://ieeexplore.ieee.org/document/10298442.
- Bringolf, Mauro (2021). Fuzz-testing SMT Solvers with Formula Weakening and Strengthening (Master Thesis thesis). ETH Zurich. doi:10.3929/ethz-b-000507582.
- ↑ 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. doi:10.1145/3484271.3484977. ISBN 978-1-4503-9088-0. https://doi.org/10.1145/3484271.3484977.
- ↑ Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana et al. (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. https://ieeexplore.ieee.org/document/8602994.
- ↑ Rungta, Neha (2022). "A Billion SMT Queries a Day (Invited Paper)". in Shoham, Sharon; Vizel, Yakir (in en). Computer Aided Verification. Lecture Notes in Computer Science. 13371. Cham: Springer International Publishing. pp. 3–18. doi:10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1. https://link.springer.com/chapter/10.1007/978-3-031-13185-1_1.
- ↑
- 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". in Majumdar, Rupak; Kunčak, Viktor (in en). Computer Aided Verification. Lecture Notes in Computer Science. 10427. Cham: Springer International Publishing. pp. 126–133. doi:10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. https://hal.archives-ouvertes.fr/hal-01669345/file/main.pdf.
- For cvc5: (Barbosa Barrett)
- 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" (in en-US). EPiC Series in Computing (EasyChair) 94: 11–22. doi:10.29007/432m. https://easychair.org/publications/paper/lNvq.
- ↑ Desharnais, Martin; Vukmirović, Petar; Blanchette, Jasmin; Wenzel, Makarius (2022). "Seventeen Provers Under the Hammer" (in en). DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8 (Schloss-Dagstuhl - Leibniz Zentrum für Informatik). doi:10.4230/LIPIcs.ITP.2022.8. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8.
- ↑ Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C Bounded Model Checker". in Ábrahám, Erika; Havelund, Klaus (in en). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. 8413. Berlin, Heidelberg: Springer. pp. 389–391. doi:10.1007/978-3-642-54862-8_26. ISBN 978-3-642-54862-8. https://link.springer.com/chapter/10.1007/978-3-642-54862-8_26.
- Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir et al. (2022). "Cvc5: A Versatile and Industrial-Strength SMT Solver". in Fisman, Dana; Rosu, Grigore (in en). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. 13243. Cham: Springer International Publishing. pp. 415–442. doi:10.1007/978-3-030-99524-9_24. ISBN 978-3-030-99524-9. https://link.springer.com/chapter/10.1007/978-3-030-99524-9_24.
- Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). "CVC4". in Gopalakrishnan, Ganesh; Qadeer, Shaz (in en). Computer Aided Verification. Lecture Notes in Computer Science. 6806. Berlin, Heidelberg: Springer. pp. 171–177. doi:10.1007/978-3-642-22110-1_14. ISBN 978-3-642-22110-1. https://link.springer.com/chapter/10.1007/978-3-642-22110-1_14.
 |  |
