Cooperating Validity Checker Explained

CVC5
Developer:Stanford University and University of Iowa
Latest Release Version:1.0.8[1]
Latest Release Date:31 August 2023
Programming Language:C++
Operating System:Windows, Linux, macOS
Genre:Theorem prover
License:BSD 3-clause

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.[2] cvc5 has bindings for C++, Python, and Java.

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

CVC4 uses the DPLL(T) architecture,[6] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,[7] floating-point arithmetic,[8] strings,[9] (co)-datatypes,[10] sequences (used to model dynamic arrays),[11] finite sets and relations,[12] [13] separation logic,[14] and uninterpreted functions among others. cvc5 additionally supports finite fields.[15]

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

cvc5 has been subject to several independent test campaigns.[17]

Applications

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

References

Notes and References

  1. Web site: Release cvc5-1.0.8 · cvc5/cvc5 . 2023-11-29 . GitHub . en.
  2. Book: 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 . Flexible Proof Production in an Industrial-Strength SMT Solver . 2022 . Blanchette . Jasmin . Kovács . Laura . Pattinson . Dirk . Automated Reasoning . https://link.springer.com/chapter/10.1007/978-3-031-10769-6_3 . Lecture Notes in Computer Science . 13385 . en . Cham . Springer International Publishing . 15–35 . 10.1007/978-3-031-10769-6_3 . 978-3-031-10769-6. 250164402 .
  3. Web site: Participants . 2023-11-29 . SMT-COMP . en-US.
  4. Web site: SMT-COMP . 2023-11-29 . SMT-COMP . en-US.
    • 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 . 10.4204/EPTCS.202.3 . 1602.01170 . 2086015 . 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 . 10.4204/EPTCS.229.13 . 1611.07627 . 440389 . 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 . 10.4204/EPTCS.260.9 . 1711.11438 . 37464992 . 2075-2180.
  6. Book: Liang . Tianyi . Reynolds . Andrew . Tinelli . Cesare . Barrett . Clark . Deters . Morgan . A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions . 2014 . Biere . Armin . Bloem . Roderick . Computer Aided Verification . https://link.springer.com/chapter/10.1007/978-3-319-08867-9_43 . Lecture Notes in Computer Science . 8559 . en . Cham . Springer International Publishing . 646–662 . 10.1007/978-3-319-08867-9_43 . 978-3-319-08867-9.
  7. Book: Hadarean . Liana . Bansal . Kshitij . Jovanović . Dejan . Barrett . Clark . Tinelli . Cesare . A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors . 2014 . Biere . Armin . Bloem . Roderick . Computer Aided Verification . https://link.springer.com/chapter/10.1007/978-3-319-08867-9_45 . Lecture Notes in Computer Science . 8559 . en . Cham . Springer International Publishing . 680–695 . 10.1007/978-3-319-08867-9_45 . 978-3-319-08867-9.
  8. Book: Brain . Martin . Niemetz . Aina . Preiner . Mathias . Reynolds . Andrew . Barrett . Clark . Tinelli . Cesare . 2019 . Dillig . Isil . Tasiran . Serdar . Invertibility Conditions for Floating-Point Formulas . Computer Aided Verification . Lecture Notes in Computer Science . en . Cham . Springer International Publishing . 116–136 . 10.1007/978-3-030-25543-5_8 . 978-3-030-25543-5. free .
  9. Book: Liang . Tianyi . Tsiskaridze . Nestan . Reynolds . Andrew . Tinelli . Cesare . Barrett . Clark . A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings . 2015 . Lutz . Carsten . Ranise . Silvio . Frontiers of Combining Systems . https://link.springer.com/chapter/10.1007/978-3-319-24246-0_9 . Lecture Notes in Computer Science . 9322 . en . Cham . Springer International Publishing . 135–150 . 10.1007/978-3-319-24246-0_9 . 978-3-319-24246-0.
  10. Book: Reynolds . Andrew . Blanchette . Jasmin Christian . A Decision Procedure for (Co)datatypes in SMT Solvers . 2015 . Felty . Amy P. . Middeldorp . Aart . Automated Deduction - CADE-25 . https://link.springer.com/chapter/10.1007/978-3-319-21401-6_13 . Lecture Notes in Computer Science . 9195 . en . Cham . Springer International Publishing . 197–213 . 10.1007/978-3-319-21401-6_13 . 978-3-319-21401-6.
  11. 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 . en . 67 . 3 . 32 . 10.1007/s10817-023-09682-2 . 261829653 . 1573-0670.
  12. Book: Bansal . Kshitij . Reynolds . Andrew . Barrett . Clark . Tinelli . Cesare . A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT . 2016 . Olivetti . Nicola . Tiwari . Ashish . Automated Reasoning . https://link.springer.com/chapter/10.1007/978-3-319-40229-1_7 . Lecture Notes in Computer Science . 9706 . en . Cham . Springer International Publishing . 82–98 . 10.1007/978-3-319-40229-1_7 . 978-3-319-40229-1.
  13. Book: Meng . Baoluo . Reynolds . Andrew . Tinelli . Cesare . Barrett . Clark . Relational Constraint Solving in SMT . 2017 . de Moura . Leonardo . Automated Deduction – CADE 26 . https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10 . Lecture Notes in Computer Science . 10395 . en . Cham . Springer International Publishing . 148–165 . 10.1007/978-3-319-63046-5_10 . 978-3-319-63046-5.
  14. Book: Reynolds . Andrew . Iosif . Radu . Serban . Cristina . King . Tim . A Decision Procedure for Separation Logic in SMT . 2016 . Artho . Cyrille . Legay . Axel . Peled . Doron . Automated Technology for Verification and Analysis . https://hal.archives-ouvertes.fr/hal-01418883/file/Atva2016-2.pdf . Lecture Notes in Computer Science . 9938 . en . Cham . Springer International Publishing . 244–261 . 10.1007/978-3-319-46520-3_16 . 978-3-319-46520-3. 6753369 .
  15. Book: Ozdemir . Alex . Kremer . Gereon . Tinelli . Cesare . Barrett . Clark . Satisfiability Modulo Finite Fields . 2023 . Enea . Constantin . Lal . Akash . Computer Aided Verification . https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8 . Lecture Notes in Computer Science . 13965 . en . Cham . Springer Nature Switzerland . 163–186 . 10.1007/978-3-031-37703-7_8 . 978-3-031-37703-7. 257235627 .
  16. Book: Reynolds . Andrew . Barbosa . Haniel . Larraz . Daniel . Tinelli . Cesare . Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis . 2020-05-30 . Automated Reasoning . Lecture Notes in Computer Science . 12166 . 141–160 . 10.1007/978-3-030-51074-9_9 . 7324138. 978-3-030-51073-2 .
    • Book: Bringolf . Mauro . Winterer . Dominik . Su . Zhendong . Finding and Understanding Incompleteness Bugs in SMT Solvers . 2023-01-05 . Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering . https://doi.org/10.1145/3551349.3560435 . ASE '22 . New York, NY, USA . Association for Computing Machinery . 1–10 . 10.1145/3551349.3560435 . 978-1-4503-9475-8. 255441416 .
    • Book: Sun . Maolin . Yang . Yibiao . Wen . Ming . Wang . Yongcong . Zhou . Yuming . Jin . Hai . Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs . 2023-07-26 . 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) . https://doi.org/10.1109/ICSE48619.2023.00018 . ICSE '23 . Melbourne, Victoria, Australia . IEEE Press . 69–81 . 10.1109/ICSE48619.2023.00018 . 978-1-6654-5701-9. 259860528 .
    • Book: Niemetz . Aina . Preiner . Mathias . Barrett . Clark . Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers . 2022 . Shoham . Sharon . Vizel . Yakir . Computer Aided Verification . https://link.springer.com/chapter/10.1007/978-3-031-13188-2_5 . Lecture Notes in Computer Science . 13372 . en . Cham . Springer International Publishing . 92–106 . 10.1007/978-3-031-13188-2_5 . 978-3-031-13188-2. 251447764 .
    • Book: Kim . Jongwook . So . Sunbeom . Oh . Hakjoo . Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations . 2023-07-26 . 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) . https://doi.org/10.1109/ICSE48619.2023.00187 . ICSE '23 . Melbourne, Victoria, Australia . IEEE Press . 2224–2236 . 10.1109/ICSE48619.2023.00187 . 978-1-6654-5701-9. 259860926 .
    • Book: SMT Solver Validation Empowered by Large Pre-Trained Language Models . https://ieeexplore.ieee.org/document/10298442 . 2023-11-29 . 10.1109/ase56229.2023.00180. 265055537 . 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE) . 2023 . Sun . Maolin . Yang . Yibiao . Wang . Yang . Wen . Ming . Jia . Haoxiang . Zhou . Yuming . 1288–1300 . 979-8-3503-2996-4 .
    • Fuzz-testing SMT Solvers with Formula Weakening and Strengthening . ETH Zurich . 2021 . Master Thesis . 10.3929/ethz-b-000507582 . en . Mauro . Bringolf.
  18. Book: Berman, Shmuel . Programming-by-example by programming-by-example: Synthesis of looping programs . 2021-10-17 . Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity . https://doi.org/10.1145/3484271.3484977 . SPLASH Companion 2021 . New York, NY, USA . Association for Computing Machinery . 19–21 . 10.1145/3484271.3484977 . 2108.08724 . 978-1-4503-9088-0. 237213485 .
  19. Book: 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 . 1–9 . 10.23919/FMCAD.2018.8602994 . 978-0-9835678-8-2. 52237693 .
  20. Book: Rungta, Neha . A Billion SMT Queries a Day (Invited Paper) . 2022 . Shoham . Sharon . Vizel . Yakir . Computer Aided Verification . https://link.springer.com/chapter/10.1007/978-3-031-13185-1_1 . Lecture Notes in Computer Science . 13371 . en . Cham . Springer International Publishing . 3–18 . 10.1007/978-3-031-13185-1_1 . 978-3-031-13185-1. 251447649 .
    • For CVC4: Book: Ekici . Burak . Mebsout . Alain . Tinelli . Cesare . Keller . Chantal . Katz . Guy . Reynolds . Andrew . Barrett . Clark . SMTCoq: A Plug-In for Integrating SMT Solvers into Coq . 2017 . Majumdar . Rupak . Kunčak . Viktor . Computer Aided Verification . https://hal.archives-ouvertes.fr/hal-01669345/file/main.pdf . Lecture Notes in Computer Science . 10427 . en . Cham . Springer International Publishing . 126–133 . 10.1007/978-3-319-63390-9_7 . 978-3-319-63390-9. 206701576 .
    • For cvc5:
    • 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 . en-US . EasyChair . 94 . 11–22 . 10.29007/432m. 259070258 . free .
  22. Desharnais . Martin . Vukmirović . Petar . Blanchette . Jasmin . Wenzel . Makarius . 2022 . Seventeen Provers Under the Hammer . DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8 . en . Schloss-Dagstuhl - Leibniz Zentrum für Informatik . 10.4230/LIPIcs.ITP.2022.8. free . 251322787 .
  23. Book: Kroening . Daniel . Tautschnig . Michael . CBMC – C Bounded Model Checker . 2014 . Ábrahám . Erika . Havelund . Klaus . Tools and Algorithms for the Construction and Analysis of Systems . https://link.springer.com/chapter/10.1007/978-3-642-54862-8_26 . Lecture Notes in Computer Science . 8413 . en . Berlin, Heidelberg . Springer . 389–391 . 10.1007/978-3-642-54862-8_26 . 978-3-642-54862-8.

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Cooperating Validity Checker".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.