Cooperating Validity Checker

From Wikipedia, the free encyclopedia
(Redirected from CVC4)
Jump to navigation Jump to search
CVC5
DevelopersStanford University and University of Iowa
Initial release2022; 4 years ago (2022)
Stable release
1.2.1[1] / January 28, 2025; 14 months ago (2025-01-28)
Repository
  • {{URL|example.com|optional display text}}Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
Written inC++
Engine
    Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
    Operating systemWindows, Linux, macOS
    TypeTheorem prover
    LicenseBSD 3-clause
    Websitecvc5.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.[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

    [edit | edit source]
    See also: Satisfiability modulo theories § 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 Rocq[24] and Isabelle.[25] CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.[26]

    References

    [edit | edit source]
    1. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    2. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    3. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    4. ^ (Barbosa et al. 2022, p. 417)
    5. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    6. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    7. ^
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    8. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    9. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    10. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    11. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    12. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    13. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    14. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    15. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    16. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    17. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    18. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    19. ^ (Barbosa et al. 2022, p. 426)
    20. ^
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    21. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    22. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    23. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    24. ^
      • For CVC4: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
      • For cvc5: (Barbosa et al. 2022, p. 425)
      • For cvc5: Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    25. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    26. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    Retrieved from "http://70.231.62.181/index.php?title=Cooperating_Validity_Checker&oldid=20148668"