Английская Википедия:Cooperating Validity Checker

Материал из Онлайн справочника
Версия от 12:45, 21 февраля 2024; EducationBot (обсуждение | вклад) (Новая страница: «{{Английская Википедия/Панель перехода}} {{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.0.8<ref>{{Cite web |title=Release cvc5-1.0.8 · cvc5/cvc5 |url=https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.8 |access-date=2023-11-29 |website=GitH...»)
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигацииПерейти к поиску

Шаблон:Short description

Шаблон:Technical Шаблон:Infobox software 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.[1] 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][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] floating-point arithmetic,[9] strings,[10] (co)-datatypes,[11] sequences (used to model dynamic arrays),[12] finite sets and relations,[13][14] separation logic,[15] and uninterpreted functions among others. cvc5 additionally supports finite fields.[16]

In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning, which is the problem of constructing a formula Шаблон:Mvar that can be conjoined with a formula Шаблон:Mvar to prove a goal formula Шаблон:Mvar.[17][18]

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

Applications

Шаблон:See also

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

References

Шаблон:Reflist

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ Шаблон:Citation
  2. ↑ Шаблон:Cite book
  3. ↑ Шаблон:Harv
  4. ↑ Шаблон:Cite web
  5. ↑ Шаблон:Cite web
  6. ↑
  7. ↑ Шаблон:Cite book
  8. ↑ Шаблон:Cite book
  9. ↑ Шаблон:Cite book
  10. ↑ Шаблон:Cite book
  11. ↑ Шаблон:Cite book
  12. ↑ Шаблон:Cite journal
  13. ↑ Шаблон:Cite book
  14. ↑ Шаблон:Cite book
  15. ↑ Шаблон:Cite book
  16. ↑ Шаблон:Cite book
  17. ↑ Шаблон:Cite book
  18. ↑ Шаблон:Harv
  19. ↑
  20. ↑ Шаблон:Cite book
  21. ↑ Шаблон:Cite book
  22. ↑ Шаблон:Cite book
  23. ↑
  24. ↑ Шаблон:Cite journal
  25. ↑ Шаблон:Cite book
Источник — http://wikihandbk.com/ruwiki/index.php?title=Английская_Википедия:Cooperating_Validity_Checker&oldid=14063847