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

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

В информатике и логике математической 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 ]} и Изабель . ^{[ 25 ]} CVC4 — это один из серверных механизмов рассуждения, поддерживаемый CBMC, средством проверки ограниченной модели C. ^{[ 26 ]}

Ссылки

^ «Выпуск cvc5-1.0.8 · cvc5/cvc5» . Гитхаб . Проверено 29 ноября 2023 г.
^ Барретт, Кларк; Тинелли, Чезаре (2018), Кларк, Эдмунд М.; Хензингер, Томас А.; Фейт, Хельмут; Блум, Родерик (ред.), «Теории выполнимости по модулю», Справочник по проверке моделей , Cham: Springer International Publishing, стр. 305–343, doi : 10.1007/978-3-319-10575-8_11 , ISBN 978-3-319-10575-8
^ Барбоза, Ханиэль; Рейнольдс, Эндрю; Кремер, Гереон; Лахнитт, Ханна; Нимец, Айна; Нётцли, Андрес; Оздемир, Алекс; Прейнер, Матиас; Вишванатан, Арджун; Витери, Скотт; Зоар, Йони; Тинелли, Чезаре; Барретт, Кларк (2022). «Гибкое производство доказательств в промышленном решателе SMT» . В Бланшетте Жасмин; Ковач, Лаура; Паттинсон, Дирк (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 13385. Чам: Springer International Publishing. стр. 15–35. дои : 10.1007/978-3-031-10769-6_3 . ISBN 978-3-031-10769-6 . S2CID 250164402 .
^ ( Барбоза и др. 2022 , стр. 417)
^ «Участники» . СМТ-КОМП . Проверено 29 ноября 2023 г.
^ «СМТ-КОМП» . СМТ-КОМП . Проверено 29 ноября 2023 г.
^
- Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (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 .
^ Лян, Тяньи; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк; Детерс, Морган (2014). «Решатель теории DPLL (T) для теории строк и регулярных выражений» . В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 646–662. дои : 10.1007/978-3-319-08867-9_43 . ISBN 978-3-319-08867-9 .
^ Хадарян, Лиана; Бансал, Кшитидж; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «Повесть о двух решателях: нетерпеливые и ленивые подходы к бит-векторам» . В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 680–695. дои : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9 .
^ Брэйн, Мартин; Нимец, Айна; Прейнер, Матиас; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2019). «Условия обратимости формул с плавающей запятой». В Диллиге, Исил; Тасиран, Сердар (ред.). Компьютерная проверка . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 116–136. дои : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5 .
^ Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решения для обычного членства и ограничений длины неограниченных строк» . В Лутце, Карстен; Ранисе, Сильвио (ред.). Границы объединения систем . Конспекты лекций по информатике. Том. 9322. Чам: Springer International Publishing. стр. 135–150. дои : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0 .
^ Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (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 .
^ Шэн, Инь; Нётцли, Андрес; Рейнольдс, Эндрю; Зоар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Джанкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15 сентября 2023 г.). «Рассуждения о векторах: выполнимость по модулю теории последовательностей» . Журнал автоматизированного рассуждения . 67 (3): 32. дои : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .
^ Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT» . В Оливетти, Никола; Тивари, Ашиш (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 9706. Чам: Springer International Publishing. стр. 82–98. дои : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1 .
^ Мэн, Баоло; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT» . В де Моура, Леонардо (ред.). Автоматический вычет – CADE 26 . Конспекты лекций по информатике. Том. 10395. Чам: Springer International Publishing. стр. 148–165. дои : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5 .
^ Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (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 .
^ Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей» . В Энее Константин; Лал, Акаш (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 13965. Чам: Springer Nature Switzerland. стр. 163–186. дои : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7 . S2CID 257235627 .
^ Рейнольдс, Эндрю; Барбоза, Ханиэль; Ларраз, Дэниел; Тинелли, Чезаре (30 мая 2020 г.). «Масштабируемые алгоритмы похищения посредством перечислительного синтеза, управляемого синтаксисом». Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 12166. стр. 141–160. дои : 10.1007/978-3-030-51074-9_9 . ISBN 978-3-030-51073-2 . ПМЦ 7324138 .
^ ( Барбоза и др. 2022 , стр. 426)
^
- Брингольф, Мауро; Винтерер, Доминик; Су, Чжэндун (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. дои : 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. дои : 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 .
^ Берман, Шмуэль (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 .
^ Бэкес, Джон; Болиньяно, Полина; Кук, Байрон; Додж, Кэтрин; Гацек, Эндрю; Луков, Каспер; Рунгта, Неха; Ткачук Оксана; Варминг, Карстен (октябрь 2018 г.). Семантическое автоматическое обоснование политик доступа AWS с использованием SMT . IEEE. стр. 1–9. дои : 10.23919/FMCAD.2018.8602994 . ISBN 978-0-9835678-8-2 . S2CID 52237693 .
^ Рунгта, Неха (2022). «Миллиард SMT-запросов в день (приглашенный доклад)» . В Шохаме, Шарон; Визель, Якир (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 13371. Чам: Springer International Publishing. стр. 3–18. дои : 10.1007/978-3-031-13185-1_1 . ISBN 978-3-031-13185-1 . S2CID 251447649 .
^
- Для 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 .
^ Дешарне, Мартин; Вукмирович, Петар; Бланшетта, жасмин; Венцель, Макариус (2022). «Семнадцать пруверов под молотком» . DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8 . Шлосс-Дагштуль — Центр компьютерных наук Лейбница. дои : 10.4230/LIPIcs.ITP.2022.8 . S2CID 251322787 .
^ Кренинг, Дэниел; Таучниг, Майкл (2014). «CBMC – средство проверки ограниченной модели C» . В Аврааме Эрика; Хавелунд, Клаус (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 8413. Берлин, Гейдельберг: Springer. стр. 389–391. дои : 10.1007/978-3-642-54862-8_26 . ISBN 978-3-642-54862-8 .

Барбоза, Ханиэль; Барретт, Кларк; Брэйн, Мартин; Кремер, Гереон; Лахнитт, Ханна; Манн, Макай; Мохамед, Абдалрахман; Мохамед, Мудатир; Нимец, Айна; Нётцли, Андрес; Оздемир, Алекс; Прейнер, Матиас; Рейнольдс, Эндрю; Шэн, Инь; Тинелли, Чезаре (2022). «Cvc5: универсальный и мощный решатель SMT» . В Фисмане, Дана; Розу, Григоре (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 13243. Чам: Springer International Publishing. стр. 415–442. дои : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9 . S2CID 247857361 .
Барретт, Кларк; Конвей, Кристофер Л.; Детерс, Морган; Хадарян, Лиана; Йованович, Деян; Кинг, Тим; Рейнольдс, Эндрю; Тинелли, Чезаре (2011). «ЦВК4» . В Гопалакришнане — Ганеша; Кадир, Шаз (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 6806. Берлин, Гейдельберг: Springer. стр. 171–177. дои : 10.1007/978-3-642-22110-1_14 . ISBN 978-3-642-22110-1 .

[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] Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (2 февраля 2016 г.). «Результаты и анализ СыГуС-Комп'15». Электронные труды по теоретической информатике . 202 : 3–26. arXiv : 1602.01170 . дои : 10.4204/EPTCS.202.3 . ISSN 2075-2180 . S2CID 2086015 .

[9] Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (22 ноября 2016 г.). «СиГуС-Комп 2016: Итоги и анализ». Электронные труды по теоретической информатике . 229 : 178–202. arXiv : 1611.07627 . дои : 10.4204/EPTCS.229.13 . ISSN 2075-2180 . S2CID 440389 .

[10] Алур, Раджив; Фисман, Дана; Сингх, Ришаб; Солар-Лезама, Армандо (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. дои : 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. дои : 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 .

[24] Брингольф, Мауро; Винтерер, Доминик; Су, Чжэндун (05 января 2023 г.). «Обнаружение и понимание ошибок неполноты в решателях SMT» . Материалы 37-й Международной конференции IEEE/ACM по автоматизированной разработке программного обеспечения . АСЭ '22. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 1–10. дои : 10.1145/3551349.3560435 . ISBN 978-1-4503-9475-8 . S2CID 255441416 .

[25] Сунь, Маолинь; Ян, Ибяо; Вэнь, Мин; Ван, Юнконг; Чжоу, Юмин; Джин, Хай (26 июля 2023 г.). «Проверка решателей SMT с помощью скелетного перечисления на основе исторических входных данных, вызывающих ошибки» . 2023 IEEE/ACM 45-я Международная конференция по программной инженерии (ICSE) . ММВБ '23. Мельбурн, Виктория, Австралия: IEEE Press. стр. 69–81. дои : 10.1109/ICSE48619.2023.00018 . ISBN 978-1-6654-5701-9 . S2CID 259860528 .

[26] Нимец, Айна; Прейнер, Матиас; Барретт, Кларк (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 .

[27] Ким, Чонвук; Итак, Санбом; О, Хакджу (26 июля 2023 г.). «Дайвер: тестирование SMT-решателя под руководством Oracle с неограниченными случайными мутациями» . 2023 IEEE/ACM 45-я Международная конференция по программной инженерии (ICSE) . ММВБ '23. Мельбурн, Виктория, Австралия: IEEE Press. стр. 2224–2236. дои : 10.1109/ICSE48619.2023.00187 . ISBN 978-1-6654-5701-9 . S2CID 259860926 .

[28] Сунь, Маолинь; Ян, Ибяо; Ван, Ян; Вэнь, Мин; Цзя, Хаосян; Чжоу, Юмин (2023). «Проверка решателя SMT на основе больших предварительно обученных языковых моделей» . 2023 г. 38-я Международная конференция IEEE/ACM по автоматизированной разработке программного обеспечения (ASE) . стр. 1288–1300. дои : 10.1109/ase56229.2023.00180 . ISBN 979-8-3503-2996-4 . S2CID 265055537 . Проверено 29 ноября 2023 г.

[29] Брингольф, Мауро (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. дои : 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 .

[34] Для 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 .

[35] Для cvc5: ( Барбоза и др. 2022 , стр. 425)

[36] Для 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 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25 ]

[ 26 ]