stringtranslate.com

Сотрудничающая программа проверки достоверности

В информатике и математической логике 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. [26]

Рекомендации

  1. ^ «Выпуск cvc5-1.0.8 · cvc5/cvc5» . Гитхаб . Проверено 29 ноября 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». В Бланшетте Жасмин; Ковач, Лаура; Паттинсон, Дирк (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 13385. Чам: Springer International Publishing. стр. 15–35. дои : 10.1007/978-3-031-10769-6_3. ISBN 978-3-031-10769-6. S2CID  250164402.
  4. ^ (Барбоса и др. 2022, стр. 417)
  5. ^ «Участники». СМТ-КОМП . Проверено 29 ноября 2023 г.
  6. ^ "СМТ-КОМП". СМТ-КОМП . Проверено 29 ноября 2023 г.
  7. ^
    • Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (2 февраля 2016 г.). «Результаты и анализ СыГуС-Комп'15». Электронные труды по теоретической информатике . 202 : 3–26. arXiv : 1602.01170 . дои : 10.4204/EPTCS.202.3. ISSN  2075-2180. S2CID  2086015.
    • Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (22 ноября 2016 г.). «СиГуС-Комп 2016: Итоги и анализ». Электронные труды по теоретической информатике . 229 : 178–202. arXiv : 1611.07627 . дои : 10.4204/EPTCS.229.13. ISSN  2075-2180. S2CID  440389.
    • Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (28 ноября 2017 г.). «СиГуС-Комп 2017: Итоги и анализ». Электронные труды по теоретической информатике . 260 : 97–115. arXiv : 1711.11438 . дои : 10.4204/EPTCS.260.9. ISSN  2075-2180. S2CID  37464992.
  8. ^ Лян, Тяньи; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк; Детерс, Морган (2014). «Решатель теории DPLL (T) для теории строк и регулярных выражений». В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 646–662. дои : 10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9.
  9. ^ Хадарян, Лиана; Бансал, Кшитидж; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «Повесть о двух решателях: нетерпеливые и ленивые подходы к бит-векторам». В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 680–695. дои : 10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
  10. ^ Брейн, Мартин; Нимец, Айна; Прейнер, Матиас; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2019). «Условия обратимости формул с плавающей запятой». В Диллиге, Исил; Тасиран, Сердар (ред.). Компьютерная проверка . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 116–136. дои : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5.
  11. ^ Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решения для обычного членства и ограничений длины неограниченных строк». В Лутце, Карстен; Ранисе, Сильвио (ред.). Границы объединения систем . Конспекты лекций по информатике. Том. 9322. Чам: Springer International Publishing. стр. 135–150. дои : 10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
  12. ^ Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (2015). «Процедура принятия решения для (Co) типов данных в решателях SMT». В Фелти, Эми П.; Мидделдорп, Аарт (ред.). Автоматизированный вычет – CADE-25 . Конспекты лекций по информатике. Том. 9195. Чам: Springer International Publishing. стр. 197–213. дои : 10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
  13. ^ Шэн, Инь; Нётцли, Андрес; Рейнольдс, Эндрю; Зоар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Джанкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15 сентября 2023 г.). «Рассуждения о векторах: выполнимость по модулю теории последовательностей». Журнал автоматизированного рассуждения . 67 (3): 32. дои : 10.1007/s10817-023-09682-2. ISSN  1573-0670. S2CID  261829653.
  14. ^ Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT». В Оливетти, Никола; Тивари, Ашиш (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 9706. Чам: Springer International Publishing. стр. 82–98. дои : 10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1.
  15. ^ Мэн, Баоло; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT». В де Моура, Леонардо (ред.). Автоматический вычет – CADE 26 . Конспекты лекций по информатике. Том. 10395. Чам: Springer International Publishing. стр. 148–165. дои : 10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5.
  16. ^ Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (2016). «Процедура принятия решения для логики разделения в SMT» (PDF) . В Арто, Сирилл; Легай, Аксель; Пелед, Дорон (ред.). Автоматизированная технология проверки и анализа . Конспекты лекций по информатике. Том. 9938. Чам: Springer International Publishing. стр. 244–261. дои : 10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. S2CID  6753369.
  17. ^ Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей». В Энее Константин; Лал, Акаш (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 13965. Чам: Springer Nature Switzerland. стр. 163–186. дои : 10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. S2CID  257235627.
  18. ^ Рейнольдс, Эндрю; Барбоза, Ханиэль; Ларраз, Дэниел; Тинелли, Чезаре (30 мая 2020 г.). «Масштабируемые алгоритмы похищения посредством перечислительного синтеза, управляемого синтаксисом». Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 12166. стр. 141–160. дои : 10.1007/978-3-030-51074-9_9. ISBN 978-3-030-51073-2. ПМЦ  7324138 .
  19. ^ (Барбоса и др. 2022, стр. 426)
  20. ^
    • Брингольф, Мауро; Винтерер, Доминик; Су, Чжэндун (05 января 2023 г.). «Обнаружение и понимание ошибок неполноты в решателях SMT». Материалы 37-й Международной конференции IEEE/ACM по автоматизированной разработке программного обеспечения . АСЭ '22. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 1–10. дои : 10.1145/3551349.3560435. ISBN 978-1-4503-9475-8. S2CID  255441416.
    • Сунь, Маолинь; Ян, Ибяо; Вэнь, Мин; Ван, Юнконг; Чжоу, Юмин; Джин, Хай (26 июля 2023 г.). «Проверка решателей SMT с помощью скелетного перечисления на основе исторических входных данных, вызывающих ошибки». 2023 IEEE/ACM 45-я Международная конференция по программной инженерии (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. Чам: Springer International Publishing. стр. 92–106. дои : 10.1007/978-3-031-13188-2_5. ISBN 978-3-031-13188-2. S2CID  251447764.
    • Ким, Чонвук; Итак, Санбом; О, Хакджу (26 июля 2023 г.). «Дайвер: тестирование SMT-решателя под руководством Oracle с неограниченными случайными мутациями». 2023 IEEE/ACM 45-я Международная конференция по программной инженерии (ICSE). ММВБ '23. Мельбурн, Виктория, Австралия: IEEE Press. стр. 2224–2236. doi : 10.1109/ICSE48619.2023.00187. ISBN 978-1-6654-5701-9. S2CID  259860926.
    • Сунь, Маолинь; Ян, Ибяо; Ван, Ян; Вэнь, Мин; Цзя, Хаосян; Чжоу, Юмин (2023). «Проверка решателя SMT на основе больших предварительно обученных языковых моделей». 2023 г. 38-я Международная конференция IEEE/ACM по автоматизированной разработке программного обеспечения (ASE) . стр. 1288–1300. дои : 10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID  265055537 . Проверено 29 ноября 2023 г.
    • Брингольф, Мауро (2021). Нечеткое тестирование SMT-решателей с ослаблением и усилением формул (магистерская диссертация). ETH Цюрих. doi : 10.3929/ethz-b-000507582.
  21. ^ Берман, Шмуэль (17 октября 2021 г.). «Программирование на примерах: синтез циклических программ». Сопутствующие материалы Международной конференции ACM SIGPLAN 2021 года по системам, программированию, языкам и приложениям: программное обеспечение для человечества . SPLASH Companion 2021. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 19–21. arXiv : 2108.08724 . дои : 10.1145/3484271.3484977. ISBN 978-1-4503-9088-0. S2CID  237213485.
  22. ^ Бэкес, Джон; Болиньяно, Полина; Кук, Байрон; Додж, Кэтрин; Гацек, Эндрю; Луков, Каспер; Рунгта, Неха; Ткачук Оксана; Варминг, Карстен (октябрь 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. дои : 10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1. S2CID  251447649.
  24. ^
    • Для CVC4: Экичи, Бурак; Мебсаут, Ален; Тинелли, Чезаре; Келлер, Шанталь; Кац, Гай; Рейнольдс, Эндрю; Барретт, Кларк (2017). «SMTCoq: плагин для интеграции решателей SMT в Coq» (PDF) . В Маджумдаре — Рупак; Кунчак, Виктор (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 10427. Чам: Springer International Publishing. стр. 126–133. дои : 10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. S2CID  206701576.
    • Для cvc5: (Барбоса и др., 2022, стр. 425)
    • Для cvc5: Барбоза, Ханиэль; Келлер, Шанталь; Рейнольдс, Эндрю; Вишванатан, Арджун; Тинелли, Чезаре; Барретт, Кларк (3 июня 2023 г.). «Интерактивная тактика SMT в Coq с использованием абдуктивного мышления». Серия EPiC по информатике . 94 . EasyChair: 11–22. дои : 10.29007/432м . 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». В Аврааме Эрика; Хавелунд, Клаус (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 8413. Берлин, Гейдельберг: Springer. стр. 389–391. дои : 10.1007/978-3-642-54862-8_26. ISBN 978-3-642-54862-8.