Сотрудничество по проверке достоверности
SMT-решатель
CVC5
Разработчик(и)Стэнфордский университет и Университет Айовы
Первоначальный выпуск2022 ; 3 года назад ( 2022 )
Стабильный релиз
1.0.8 [1] / 31 августа 2023 г.
Написано вС++
Операционная системаWindows , Linux , MacOS
ТипДоказательство теорем
ЛицензияBSD 3-пункт
Веб-сайтcvc5.github.io

В информатике и математической логике Cooperating Validity Checker (CVC) — это семейство решателей выполнимости по модулю теорий (SMT). Последние основные версии CVC — CVC4 и CVC5 (стилизованные под cvc5); более ранние версии включают CVC, CVC Lite и CVC3. [2] Как CVC4, так и cvc5 поддерживают форматы ввода SMT-LIB и TPTP для решения задач SMT, а также формат SyGuS-IF для синтеза программ . Как CVC4, так и cvc5 могут выводить доказательства, которые можно независимо проверить в формате LFSC, cvc5 дополнительно поддерживает форматы Alethe и Lean 4. [3] [4] cvc5 имеет привязки для C++ , Python и Java .

CVC4 участвовал в SMT-COMP в 2014–2020 годах [5], а cvc5 участвовал в 2021–2022 годах [6] . CVC4 участвовал в SyGuS-COMP в 2015–2019 годах [7] и в CASC в 2013–2015 годах.

CVC4 использует архитектуру DPLL(T) [8] и поддерживает теории линейной арифметики над рациональными и целыми числами , битовые векторы фиксированной ширины, [9] арифметику с плавающей точкой , [10] строки , [11] (co)-типы данных , [12] последовательности (используемые для моделирования динамических массивов ), [13] конечные множества и отношения , [14] [15] логику разделения , [16] и неинтерпретируемые функции среди прочих. cvc5 дополнительно поддерживает конечные поля . [17]

В дополнение к стандартным решениям SMT и SyGuS, cvc5 поддерживает абдуктивное рассуждение , которое представляет собой задачу построения формулы B , которую можно объединить с формулой A для доказательства целевой формулы C. [18] [19]

cvc5 был подвергнут нескольким независимым тестовым кампаниям. [20]

Приложения

CVC4 применялся для синтеза рекурсивных программ [21] и для проверки политик доступа Amazon Web Services [22] [23] CVC4 и cvc5 были интегрированы с Coq [24] и Isabelle [25] CVC4 является одним из внутренних рассуждений, поддерживаемых CBMC, C Bounded Model Checker [26]

Ссылки

  1. ^ "Выпуск cvc5-1.0.8 · cvc5/cvc5". GitHub . Получено 29.11.2023 .
  2. ^ Барретт, Кларк; Тинелли, Чезаре (2018), Кларк, Эдмунд М.; Хензингер, Томас А.; Вайт, Хельмут; Блюм, Родерик (ред.), «Теории выполнимости по модулю», Справочник по проверке моделей , Cham: Springer International Publishing, стр.  305–343 , doi : 10.1007/978-3-319-10575-8_11 , ISBN 978-3-319-10575-8
  3. ^ Барбоза, Ханиэль; Рейнольдс, Эндрю; Кремер, Гереон; Лахнитт, Ханна; Нимец, Айна; Нётцли, Андрес; Оздемир, Алекс; Прейнер, Матиас; Вишванатан, Арджун; Витери, Скотт; Зохар, Йони; Тинелли, Чезаре; Барретт, Кларк (2022). «Гибкое производство доказательств в промышленном решателе SMT». В Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (ред.). Автоматизированное рассуждение . Конспект лекций по информатике. Том 13385. Cham: Springer International Publishing. стр.  15–35 . doi :10.1007/978-3-031-10769-6_3. ISBN 978-3-031-10769-6. S2CID  250164402.
  4. ^ (Барбоса и др. 2022, стр. 417)
  5. ^ "Участники". SMT-COMP . Получено 29.11.2023 .
  6. ^ "SMT-COMP". SMT-COMP . Получено 29.11.2023 .
  7. ^
    • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Результаты и анализ 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: результаты и анализ". 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 (28.11.2017). "SyGuS-Comp 2017: результаты и анализ". Electronic Proceedings in Theoretical Computer Science . 260 : 97–115 . arXiv : 1711.11438 . doi :10.4204/EPTCS.260.9. ISSN  2075-2180. S2CID  37464992.
  8. ^ Лян, Тяньи; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк; Детерс, Морган (2014). "Решатель теории DPLL(T) для теории строк и регулярных выражений". В Biere, Armin; Bloem, Roderick (ред.). 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.
  9. ^ Хадареан, Лиана; Бансал, Кшитий; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «История двух решателей: энергичные и ленивые подходы к бит-векторам». В Бире, Армин; Блюм, Родерик (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 8559. Cham: Springer International Publishing. стр.  680– 695. doi :10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
  10. ^ Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). «Условия обратимости формул с плавающей точкой». В Dillig, Isil; Tasiran, Serdar (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. стр.  116– 136. doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5.
  11. ^ Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решений для регулярного членства и ограничений длины для неограниченных строк». В Lutz, Carsten; Ranise, Silvio (ред.). 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.
  12. ^ Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (2015). «Процедура принятия решения для (Co)типов данных в SMT-решателях». В Фелти, Эми П.; Миддельдорп, Аарт (ред.). Автоматизированная дедукция — CADE-25 . Конспект лекций по информатике. Том 9195. Cham: Springer International Publishing. стр.  197– 213. doi :10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
  13. ^ Шэн, Ин; Нётцли, Андрес; Рейнольдс, Эндрю; Зохар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Юнкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15.09.2023). «Рассуждения о векторах: выполнимость по модулю теории последовательностей». Журнал автоматизированного рассуждения . 67 (3): 32. doi :10.1007/s10817-023-09682-2. ISSN  1573-0670. S2CID  261829653.
  14. ^ Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT». В Olivetti, Nicola; Tiwari, Ashish (ред.). Автоматизированное рассуждение . Конспект лекций по информатике. Том 9706. Cham: Springer International Publishing. стр.  82–98 . doi :10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1.
  15. ^ Мэн, Баолуо; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT». Ин де Моура, Леонардо (ред.). Автоматизированная дедукция – CADE 26. Конспект лекций по информатике. Том 10395. Cham: Springer International Publishing. стр.  148– 165. doi :10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5.
  16. ^ Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (2016). "Процедура принятия решений для логики разделения в SMT" (PDF) . В Artho, Сирилл; Легай, Аксель; Пелед, Дорон (ред.). Автоматизированная технология проверки и анализа . Конспект лекций по информатике. Том 9938. Cham: Springer International Publishing. стр.  244– 261. doi : 10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. S2CID  6753369.
  17. ^ Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей». В Энеа, Константин; Лал, Акаш (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 13965. Cham: Springer Nature Switzerland. стр.  163–186 . doi :10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. S2CID  257235627.
  18. ^ Рейнольдс, Эндрю; Барбоза, Ханиэль; Ларраз, Даниэль; Тинелли, Чезаре (2020-05-30). «Масштабируемые алгоритмы для абдукции с помощью синтеза, управляемого перечислительным синтаксисом». Автоматизированное рассуждение . Конспект лекций по информатике. Том 12166. С.  141– 160. doi :10.1007/978-3-030-51074-9_9. ISBN 978-3-030-51073-2. ЧМЦ  7324138 .
  19. ^ (Барбоса и др. 2022, стр. 426)
  20. ^
    • Брингольф, Мауро; Винтерер, Доминик; Су, Чжэндун (2023-01-05). «Поиск и понимание ошибок неполноты в решателях SMT». Труды 37-й Международной конференции IEEE/ACM по автоматизированной программной инженерии . ASE '22. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр.  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). «Проверка решателей SMT с помощью перечисления скелетов, усиленного историческими входными данными, вызывающими ошибки». IEEE/ACM 45-я Международная конференция по программной инженерии (ICSE) 2023 года . ICSE '23. Мельбурн, Виктория, Австралия: IEEE Press. стр.  69–81 . doi :10.1109/ICSE48619.2023.00018. ISBN 978-1-6654-5701-9. S2CID  259860528.
    • Нимец, Айна; Прейнер, Матиас; Барретт, Кларк (2022). «Murxla: модульный и высокорасширяемый API-фаззер для SMT-решателей». В Шохам, Шарон; Визель, Якир (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 13372. Cham: Springer International Publishing. стр.  92–106 . doi :10.1007/978-3-031-13188-2_5. ISBN 978-3-031-13188-2. S2CID  251447764.
    • Ким, Чонвук; Со, Санбом; О, Хакджу (2023-07-26). «Дайвер: Тестирование решателя SMT под руководством Oracle с неограниченными случайными мутациями». 45-я международная конференция IEEE/ACM по программной инженерии (ICSE) 2023 года. ICSE '23. Мельбурн, Виктория, Австралия: IEEE Press. стр.  2224– 2236. doi : 10.1109/ICSE48619.2023.00187. ISBN 978-1-6654-5701-9. S2CID  259860926.
    • Сан, Маолинь; Ян, Ибяо; Ван, Ян; Вэнь, Мин; Цзя, Хаосян; Чжоу, Юймин (2023). «Проверка решателя SMT с помощью больших предварительно обученных языковых моделей». 38-я Международная конференция IEEE/ACM по автоматизированной программной инженерии (ASE) 2023 г. стр.  1288–1300 . doi :10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID  265055537 . Получено 29.11.2023 .
    • Брингольф, Мауро (2021). Fuzz-тестирование SMT-решателей с ослаблением и усилением формул (магистерская диссертация). ETH Zurich. doi : 10.3929/ethz-b-000507582.
  21. ^ Берман, Шмуэль (17.10.2021). «Программирование по примеру с помощью программирования по примеру: синтез циклических программ». Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity . SPLASH Companion 2021. Нью-Йорк, Нью-Йорк, США: Association for Computing Machinery. стр.  19–21 . arXiv : 2108.08724 . doi :10.1145/3484271.3484977. ISBN 978-1-4503-9088-0. S2CID  237213485.
  22. ^ Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (октябрь 2018 г.). Автоматизированное обоснование на основе семантики для политик доступа AWS с использованием SMT. IEEE. стр.  1– 9. doi :10.23919/FMCAD.2018.8602994. ISBN 978-0-9835678-8-2. S2CID  52237693.
  23. ^ Рунгта, Неха (2022). «Миллиард запросов SMT в день (приглашенный доклад)». В Шохам, Шарон; Визель, Якир (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 13371. Чам: Springer International Publishing. стр.  3–18 . doi :10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1. S2CID  251447649.
  24. ^
    • Для CVC4: Экичи, Бурак; Мебсоут, Ален; Тинелли, Чезаре; Келлер, Шанталь; Кац, Гай; Рейнольдс, Эндрю; Барретт, Кларк (2017). "SMTCoq: плагин для интеграции SMT-решателей в Coq" (PDF) . В Маджумдар, Рупак; Кунчак, Виктор (ред.). Компьютерная проверка . Конспект лекций по информатике. Том 10427. Cham: Springer International Publishing. стр.  126– 133. doi : 10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. S2CID  206701576.
    • Для cvc5: (Барбоса и др., 2022, стр. 425)
    • Для cvc5: Барбоза, Ханиэль; Келлер, Шанталь; Рейнольдс, Эндрю; Вишванатан, Арджун; Тинелли, Чезаре; Барретт, Кларк (2023-06-03). «Интерактивная тактика SMT в Coq с использованием абдуктивного рассуждения». Серия EPiC по вычислениям . 94. EasyChair: 11– 22. doi : 10.29007/432m . S2CID  259070258.
  25. ^ Дешарне, Мартин; Вукмирович, Петар; Бланшетт, Жасмин; Венцель, Макариус (2022). «Семнадцать пруверов под молотом». DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8 . Шлосс-Дагштуль - Центр информатики Лейбница. дои : 10.4230/LIPIcs.ITP.2022.8 . S2CID  251322787.
  26. ^ Крёнинг, Даниэль; Таучниг, Михаэль (2014). "CBMC – C Bounded Model Checker". В Ábrahám, Эрика; Хавелунд, Клаус (ред.). Инструменты и алгоритмы для построения и анализа систем . Конспект лекций по информатике. Том 8413. Берлин, Гейдельберг: 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). "Cvc5: универсальный и промышленный решатель SMT". В Fisman, Dana; Rosu, Grigore (ред.). Инструменты и алгоритмы для построения и анализа систем . Конспект лекций по информатике. Том 13243. Cham: Springer International Publishing. стр.  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". В Gopalakrishnan, Ganesh; Qadeer, Shaz (ред.). 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.
Получено с "https://en.wikipedia.org/w/index.php?title=Cooperating_Validity_Checker&oldid=1237250770"