From Wikipedia, the free encyclopedia
SMT solver
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" . GitHub . Retrieved 2023-11-29 .
^ 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
^ 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 .
^ (
Barbosa et al. 2022 , p. 417)
^
"Participants" . SMT-COMP . Retrieved 2023-11-29 .
^
"SMT-COMP" . SMT-COMP . Retrieved 2023-11-29 .
^
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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ 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 .
^ (
Barbosa et al. 2022 , p. 426)
^
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 .
^ 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 .
^ 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 .
^ 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 .
^
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 .
^ 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 .
^ 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 .