Cooperating Validity Checker

{{Short description|SMT solver}}

{{Technical|date=November 2023}}

{{Infobox software

| name = CVC5

| developer = Stanford University and University of Iowa

| released = {{Start date and age|2022}}

| latest release version = 1.2.1{{Cite web |title=Release cvc5-1.2.1 · cvc5/cvc5 |url=https://github.com/cvc5/cvc5/releases/tag/cvc5-1.2.1 |access-date=2025-02-12 |website=GitHub |language=en}}

| latest release date = {{Start date and age|2025|01|28}}

| programming language = C++

| operating system = Windows, Linux, macOS

| genre = Theorem prover

| license = BSD 3-clause

| website = {{URL|https://cvc5.github.io/}}

}}

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.{{Citation |last1=Barrett |first1=Clark |title=Satisfiability Modulo Theories |date=2018 |work=Handbook of Model Checking |pages=305–343 |editor-last=Clarke |editor-first=Edmund M. |place=Cham |publisher=Springer International Publishing |language=en |doi=10.1007/978-3-319-10575-8_11 |isbn=978-3-319-10575-8 |last2=Tinelli |first2=Cesare |editor2-last=Henzinger |editor2-first=Thomas A. |editor3-last=Veith |editor3-first=Helmut |editor4-last=Bloem |editor4-first=Roderick|doi-access=free }} 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.{{Cite book |last1=Barbosa |first1=Haniel |last2=Reynolds |first2=Andrew |last3=Kremer |first3=Gereon |last4=Lachnitt |first4=Hanna |last5=Niemetz |first5=Aina |last6=Nötzli |first6=Andres |last7=Ozdemir |first7=Alex |last8=Preiner |first8=Mathias |last9=Viswanathan |first9=Arjun |last10=Viteri |first10=Scott |last11=Zohar |first11=Yoni |last12=Tinelli |first12=Cesare |last13=Barrett |first13=Clark |chapter=Flexible Proof Production in an Industrial-Strength SMT Solver |date=2022 |editor-last=Blanchette |editor-first=Jasmin |editor2-last=Kovács |editor2-first=Laura |editor3-last=Pattinson |editor3-first=Dirk |title=Automated Reasoning |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-10769-6_3 |series=Lecture Notes in Computer Science |volume=13385 |language=en |location=Cham |publisher=Springer International Publishing |pages=15–35 |doi=10.1007/978-3-031-10769-6_3 |isbn=978-3-031-10769-6|s2cid=250164402 }}{{harv|Barbosa|Barrett|Brain|Kremer|2022|p=417}} cvc5 has bindings for C++, Python, and Java.

CVC4 competed in SMT-COMP in the years 2014-2020,{{Cite web |title=Participants |url=https://smt-comp.github.io/2014/participants.html |access-date=2023-11-29 |website=SMT-COMP |language=en-US}} and cvc5 has competed in the years 2021-2022.{{Cite web |title=SMT-COMP |url=https://smt-comp.github.io/2022/participants.html |access-date=2023-11-29 |website=SMT-COMP |language=en-US}} CVC4 competed in SyGuS-COMP in the years 2015-2019,

• {{Cite journal |last1=Alur |first1=Rajeev |last2=Fisman |first2=Dana |last3=Singh |first3=Rishabh |last4=Solar-Lezama |first4=Armando |date=2016-02-02 |title=Results and Analysis of SyGuS-Comp'15 |journal=Electronic Proceedings in Theoretical Computer Science |volume=202 |pages=3–26 |doi=10.4204/EPTCS.202.3 |arxiv=1602.01170 |s2cid=2086015 |issn=2075-2180}}
• {{Cite journal |last1=Alur |first1=Rajeev |last2=Fisman |first2=Dana |last3=Singh |first3=Rishabh |last4=Solar-Lezama |first4=Armando |date=2016-11-22 |title=SyGuS-Comp 2016: Results and Analysis |journal=Electronic Proceedings in Theoretical Computer Science |volume=229 |pages=178–202 |doi=10.4204/EPTCS.229.13 |arxiv=1611.07627 |s2cid=440389 |issn=2075-2180}}
• {{Cite journal |last1=Alur |first1=Rajeev |last2=Fisman |first2=Dana |last3=Singh |first3=Rishabh |last4=Solar-Lezama |first4=Armando |date=2017-11-28 |title=SyGuS-Comp 2017: Results and Analysis |journal=Electronic Proceedings in Theoretical Computer Science |volume=260 |pages=97–115 |doi=10.4204/EPTCS.260.9 |arxiv=1711.11438 |s2cid=37464992 |issn=2075-2180}} and in CASC in 2013-2015.

CVC4 uses the DPLL(T) architecture,{{Cite book |last1=Liang |first1=Tianyi |last2=Reynolds |first2=Andrew |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |last5=Deters |first5=Morgan |chapter=A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions |date=2014 |editor-last=Biere |editor-first=Armin |editor2-last=Bloem |editor2-first=Roderick |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-08867-9_43 |series=Lecture Notes in Computer Science |volume=8559 |language=en |location=Cham |publisher=Springer International Publishing |pages=646–662 |doi=10.1007/978-3-319-08867-9_43 |isbn=978-3-319-08867-9}} and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,{{Cite book |last1=Hadarean |first1=Liana |last2=Bansal |first2=Kshitij |last3=Jovanović |first3=Dejan |last4=Barrett |first4=Clark |last5=Tinelli |first5=Cesare |chapter=A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors |date=2014 |editor-last=Biere |editor-first=Armin |editor2-last=Bloem |editor2-first=Roderick |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-08867-9_45 |series=Lecture Notes in Computer Science |volume=8559 |language=en |location=Cham |publisher=Springer International Publishing |pages=680–695 |doi=10.1007/978-3-319-08867-9_45 |isbn=978-3-319-08867-9}} floating-point arithmetic,{{Cite book |last1=Brain |first1=Martin |last2=Niemetz |first2=Aina |last3=Preiner |first3=Mathias |last4=Reynolds |first4=Andrew |last5=Barrett |first5=Clark |last6=Tinelli |first6=Cesare |date=2019 |editor-last=Dillig |editor-first=Isil |editor2-last=Tasiran |editor2-first=Serdar |chapter=Invertibility Conditions for Floating-Point Formulas |title=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=116–136 |doi=10.1007/978-3-030-25543-5_8 |isbn=978-3-030-25543-5|doi-access=free }} strings,{{Cite book |last1=Liang |first1=Tianyi |last2=Tsiskaridze |first2=Nestan |last3=Reynolds |first3=Andrew |last4=Tinelli |first4=Cesare |last5=Barrett |first5=Clark |chapter=A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings |date=2015 |editor-last=Lutz |editor-first=Carsten |editor2-last=Ranise |editor2-first=Silvio |title=Frontiers of Combining Systems |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-24246-0_9 |series=Lecture Notes in Computer Science |volume=9322 |language=en |location=Cham |publisher=Springer International Publishing |pages=135–150 |doi=10.1007/978-3-319-24246-0_9 |isbn=978-3-319-24246-0}} (co)-datatypes,{{Cite book |last1=Reynolds |first1=Andrew |last2=Blanchette |first2=Jasmin Christian |chapter=A Decision Procedure for (Co)datatypes in SMT Solvers |date=2015 |editor-last=Felty |editor-first=Amy P. |editor2-last=Middeldorp |editor2-first=Aart |title=Automated Deduction - CADE-25 |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-21401-6_13 |series=Lecture Notes in Computer Science |volume=9195 |language=en |location=Cham |publisher=Springer International Publishing |pages=197–213 |doi=10.1007/978-3-319-21401-6_13 |isbn=978-3-319-21401-6}} sequences (used to model dynamic arrays),{{Cite journal |last1=Sheng |first1=Ying |last2=Nötzli |first2=Andres |last3=Reynolds |first3=Andrew |last4=Zohar |first4=Yoni |last5=Dill |first5=David |last6=Grieskamp |first6=Wolfgang |last7=Park |first7=Junkil |last8=Qadeer |first8=Shaz |last9=Barrett |first9=Clark |last10=Tinelli |first10=Cesare |date=2023-09-15 |title=Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences |url=https://doi.org/10.1007/s10817-023-09682-2 |journal=Journal of Automated Reasoning |language=en |volume=67 |issue=3 |pages=32 |doi=10.1007/s10817-023-09682-2 |s2cid=261829653 |issn=1573-0670}} finite sets and relations,{{Cite book |last1=Bansal |first1=Kshitij |last2=Reynolds |first2=Andrew |last3=Barrett |first3=Clark |last4=Tinelli |first4=Cesare |chapter=A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT |date=2016 |editor-last=Olivetti |editor-first=Nicola |editor2-last=Tiwari |editor2-first=Ashish |title=Automated Reasoning |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-40229-1_7 |series=Lecture Notes in Computer Science |volume=9706 |language=en |location=Cham |publisher=Springer International Publishing |pages=82–98 |doi=10.1007/978-3-319-40229-1_7 |isbn=978-3-319-40229-1}}{{Cite book |last1=Meng |first1=Baoluo |last2=Reynolds |first2=Andrew |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |chapter=Relational Constraint Solving in SMT |date=2017 |editor-last=de Moura |editor-first=Leonardo |title=Automated Deduction – CADE 26 |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10 |series=Lecture Notes in Computer Science |volume=10395 |language=en |location=Cham |publisher=Springer International Publishing |pages=148–165 |doi=10.1007/978-3-319-63046-5_10 |isbn=978-3-319-63046-5}} separation logic,{{Cite book |last1=Reynolds |first1=Andrew |last2=Iosif |first2=Radu |last3=Serban |first3=Cristina |last4=King |first4=Tim |chapter=A Decision Procedure for Separation Logic in SMT |date=2016 |editor-last=Artho |editor-first=Cyrille |editor2-last=Legay |editor2-first=Axel |editor3-last=Peled |editor3-first=Doron |title=Automated Technology for Verification and Analysis |chapter-url=https://hal.archives-ouvertes.fr/hal-01418883/file/Atva2016-2.pdf |series=Lecture Notes in Computer Science |volume=9938 |language=en |location=Cham |publisher=Springer International Publishing |pages=244–261 |doi=10.1007/978-3-319-46520-3_16 |isbn=978-3-319-46520-3|s2cid=6753369 }} and uninterpreted functions among others. cvc5 additionally supports finite fields.{{Cite book |last1=Ozdemir |first1=Alex |last2=Kremer |first2=Gereon |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |chapter=Satisfiability Modulo Finite Fields |date=2023 |editor-last=Enea |editor-first=Constantin |editor2-last=Lal |editor2-first=Akash |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8 |series=Lecture Notes in Computer Science |volume=13965 |language=en |location=Cham |publisher=Springer Nature Switzerland |pages=163–186 |doi=10.1007/978-3-031-37703-7_8 |isbn=978-3-031-37703-7|s2cid=257235627 }}

In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning, which is the problem of constructing a formula {{mvar|B}} that can be conjoined with a formula {{mvar|A}} to prove a goal formula {{mvar|C}}.{{Cite book |last1=Reynolds |first1=Andrew |last2=Barbosa |first2=Haniel |last3=Larraz |first3=Daniel |last4=Tinelli |first4=Cesare |chapter=Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis |date=2020-05-30 |title=Automated Reasoning |series=Lecture Notes in Computer Science |volume=12166 |pages=141–160 |doi=10.1007/978-3-030-51074-9_9 |pmc=7324138|isbn=978-3-030-51073-2 }}{{harv|Barbosa|Barrett|Brain|Kremer|2022|p=426}}

cvc5 has been subject to several independent test campaigns.

• {{Cite book |last1=Bringolf |first1=Mauro |last2=Winterer |first2=Dominik |last3=Su |first3=Zhendong |chapter=Finding and Understanding Incompleteness Bugs in SMT Solvers |date=2023-01-05 |title=Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering |chapter-url=https://doi.org/10.1145/3551349.3560435 |series=ASE '22 |location=New York, NY, USA |publisher=Association for Computing Machinery |pages=1–10 |doi=10.1145/3551349.3560435 |isbn=978-1-4503-9475-8|s2cid=255441416 }}
• {{Cite book |last1=Sun |first1=Maolin |last2=Yang |first2=Yibiao |last3=Wen |first3=Ming |last4=Wang |first4=Yongcong |last5=Zhou |first5=Yuming |last6=Jin |first6=Hai |chapter=Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs |date=2023-07-26 |title=2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) |chapter-url=https://doi.org/10.1109/ICSE48619.2023.00018 |series=ICSE '23 |location=Melbourne, Victoria, Australia |publisher=IEEE Press |pages=69–81 |doi=10.1109/ICSE48619.2023.00018 |isbn=978-1-6654-5701-9|s2cid=259860528 }}
• {{Cite book |last1=Niemetz |first1=Aina |last2=Preiner |first2=Mathias |last3=Barrett |first3=Clark |chapter=Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers |date=2022 |editor-last=Shoham |editor-first=Sharon |editor2-last=Vizel |editor2-first=Yakir |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-13188-2_5 |series=Lecture Notes in Computer Science |volume=13372 |language=en |location=Cham |publisher=Springer International Publishing |pages=92–106 |doi=10.1007/978-3-031-13188-2_5 |isbn=978-3-031-13188-2|s2cid=251447764 }}
• {{Cite book |last1=Kim |first1=Jongwook |last2=So |first2=Sunbeom |last3=Oh |first3=Hakjoo |chapter=Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations |date=2023-07-26 |title=2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) |chapter-url=https://doi.org/10.1109/ICSE48619.2023.00187 |series=ICSE '23 |location=Melbourne, Victoria, Australia |publisher=IEEE Press |pages=2224–2236 |doi=10.1109/ICSE48619.2023.00187 |isbn=978-1-6654-5701-9|s2cid=259860926 |url=https://zenodo.org/record/7632205 }}
• {{Cite book |chapter=SMT Solver Validation Empowered by Large Pre-Trained Language Models |chapter-url=https://ieeexplore.ieee.org/document/10298442 |access-date=2023-11-29 |doi=10.1109/ase56229.2023.00180|s2cid=265055537 |title=2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE) |date=2023 |last1=Sun |first1=Maolin |last2=Yang |first2=Yibiao |last3=Wang |first3=Yang |last4=Wen |first4=Ming |last5=Jia |first5=Haoxiang |last6=Zhou |first6=Yuming |pages=1288–1300 |isbn=979-8-3503-2996-4 }}
• {{Cite thesis |title=Fuzz-testing SMT Solvers with Formula Weakening and Strengthening |url=https://www.research-collection.ethz.ch/handle/20.500.11850/507582 |publisher=ETH Zurich |date=2021 |degree=Master Thesis |doi=10.3929/ethz-b-000507582 |language=en |first=Mauro |last=Bringolf}}