Jump to content

Cooperating Validity Checker

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by RichBot (talk | contribs) at 22:25, 29 November 2023 ((Beep, Boop). I have removed a template which is not valid in Draftspace). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
CVC5
Developer(s)Stanford University and University of Iowa
Initial release2022; 3 years ago (2022)
Stable release
1.0.8[1] / 31 August 2023
Written inC++
Operating systemWindows, Linux, macOS
TypeTheorem prover
LicenseBSD 3-clause
Websitecvc5.github.io

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

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

CVC4 uses the DPLL(T) architecture,[7] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,[8] strings,[9] (co)-datatypes,[10] sequences, finite sets and relations, separation logic, and uninterpreted functions among others.

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.[11][12]

Applications

See also: Satisfiability modulo theories § Applications

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

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, retrieved 2023-11-29
  3. ^ (Barbosa, Barrett & Brain, p. 417)
  4. ^ "Participants". SMT-COMP. Retrieved 2023-11-29.
  5. ^ "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.
  6. ^
  7. ^ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). Biere, Armin; Bloem, Roderick (eds.). "A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9.
  8. ^ Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). Biere, Armin; Bloem, Roderick (eds.). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
  9. ^ Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). Lutz, Carsten; Ranise, Silvio (eds.). "A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings". Frontiers of Combining Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
  10. ^ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). Felty, Amy P.; Middeldorp, Aart (eds.). "A Decision Procedure for (Co)datatypes in SMT Solvers". Automated Deduction - CADE-25. Lecture Notes in Computer Science. Cham: Springer International Publishing: 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
  11. ^ Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis". Automated Reasoning. 12166: 141–160. doi:10.1007/978-3-030-51074-9_9. PMC 7324138.
  12. ^ (Barbosa, Barrett & Brain, p. 426)
  13. ^ 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: 19–21. doi:10.1145/3484271.3484977. ISBN 978-1-4503-9088-0.
  14. ^ Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (2018-10). "Semantic-based Automated Reasoning for AWS Access Policies using SMT". IEEE: 1–9. doi:10.23919/FMCAD.2018.8602994. ISBN 978-0-9835678-8-2. {{cite journal}}: Check date values in: |date= (help); Cite journal requires |journal= (help)
  15. ^ Rungta, Neha (2022). Shoham, Sharon; Vizel, Yakir (eds.). "A Billion SMT Queries a Day (Invited Paper)". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 3–18. doi:10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1. {{cite journal}}: no-break space character in |title= at position 24 (help)
  16. ^ Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). Majumdar, Rupak; Kunčak, Viktor (eds.). "SMTCoq: A Plug-In for Integrating SMT Solvers into Coq". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 126–133. doi:10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9.
  17. ^ (Barbosa, Barrett & Brain, p. 425)
  18. ^ Kroening, Daniel; Tautschnig, Michael (2014). Ábrahám, Erika; Havelund, Klaus (eds.). "CBMC – C Bounded Model Checker". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 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). Fisman, Dana; Rosu, Grigore (eds.). "cvc5: A Versatile and Industrial-Strength SMT Solver". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 415–442. doi:10.1007/978-3-030-99524-9_24. ISBN 978-3-030-99524-9.
  • Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). "CVC4". Computer Aided Verification. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 171–177. doi:10.1007/978-3-642-22110-1_14. ISBN 978-3-642-22110-1.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Cooperating_Validity_Checker&oldid=1187540406"