Проверка модели BLAST

ВЗРЫВ
Оригинальный автор(ы)	Дирк Бейер, Томас Хензингер, Ранджит Джала, Рупак Маджумдар, Беркли
Разработчик(и)	Михаил Мандрыкин, Вадим Мутилин, Павел Швед, Институт системного программирования
Стабильный релиз	2.7.3 / 30 октября 2015 г. ; 8 лет назад ( 2015-10-30 )
Написано в	OCaml
Операционная система	Линукс
Тип	Статический анализ кода
Лицензия	Лицензия Apache, версия 2.0
Веб-сайт	forge.ispras.ru/projects/blast

Berkeley Lazy Abstraction Software verification Tool ( BLAST ) — это инструмент проверки моделей программного обеспечения для программ на языке C. Задача, решаемая BLAST, заключается в необходимости проверки того, удовлетворяет ли программное обеспечение поведенческим требованиям связанных с ним интерфейсов. BLAST использует автоматическое уточнение абстракции на основе контрпримера для построения абстрактной модели, которая затем проверяется на предмет свойств безопасности. Абстракция строится « на лету » и только с требуемой точностью .

Достижения

BLAST занял первое место в категории DeviceDrivers64 на 1-м конкурсе по верификации программного обеспечения (2012), который проводился на выставке TACAS 2012 в Таллинне . ^[2]

BLAST занял третье место (категория DeviceDrivers64) на 2-м конкурсе по верификации программного обеспечения (2013), который проводился на выставке TACAS 2013 в Риме . ^[3]

BLAST занял первое место в категории DeviceDrivers64 на 3-м конкурсе по верификации программного обеспечения (2014), который проводился на выставке TACAS 2014 в Гренобле . ^[4]

Ссылки

^ «Файлы - BLAST - Проекты с открытым исходным кодом».
^ Дирк Бейер (2012). "Конкурс по верификации программного обеспечения (SV-COMP)" (PDF) . Труды 18-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.
^ Дирк Бейер (2013). "Второй конкурс по верификации программного обеспечения (резюме SV-COMP 2013)" (PDF) . Труды 19-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.
^ Дирк Бейер (2014). "Третий конкурс по верификации программного обеспечения (резюме SV-COMP 2014)" (PDF) . Труды 20-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.

Примечания

Павел Швед; Михаил Мандрыкин; Вадим Мутилин (2012). "Анализ предикатов с BLAST 2.7.". В Фланаган, Кормак; Кёниг, Барбара (ред.). Инструменты и алгоритмы для построения и анализа систем . Конспект лекций по информатике. Том 7214. Springer-Verlag. С. 525–527. ISBN 978-3-642-28756-5.

Бейер, Дирк; Хензингер, Томас А.; Джала, Ранджит; Маджумдар, Рупак (2007). «Проверка программных моделей Blast». Международный журнал по программным инструментам для передачи технологий . 9 (5–6): 505–525. doi :10.1007/s10009-007-0044-z. S2CID 1662778.
Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar & Gregoire Sutre (2003). "Проверка программного обеспечения с помощью Blast". В Ball, Thomas & Rajamani, Sriram K. (ред.). Труды 10-го семинара SPIN по проверке программного обеспечения для моделирования (SPIN 2003) . Конспект лекций по информатике. Том 2648. Springer-Verlag. С. 235–239. ISBN 3-540-40117-2.

Внешние ссылки

Веб-сайт BLAST 2.5
Веб-сайт BLAST 2.7

Эта статья, связанная с программированием, является заглушкой . Вы можете помочь Википедии, расширив ее.

[1] «Файлы - BLAST - Проекты с открытым исходным кодом».

[2] Дирк Бейер (2012). "Конкурс по верификации программного обеспечения (SV-COMP)" (PDF) . Труды 18-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.

[3] Дирк Бейер (2013). "Второй конкурс по верификации программного обеспечения (резюме SV-COMP 2013)" (PDF) . Труды 19-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.

[4] Дирк Бейер (2014). "Третий конкурс по верификации программного обеспечения (резюме SV-COMP 2014)" (PDF) . Труды 20-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.