Проверка модели BLAST
| Оригинальный автор(ы) | Дирк Бейер, Томас Хензингер, Ранджит Джала, Рупак Маджумдар, Беркли |
|---|---|
| Разработчик(и) | Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming |
| Стабильная версия | 2.7.3 [1] / 30 октября 2015 г |
| Написано в | OCaml |
| Операционная система | Линукс |
| Тип | Статический анализ кода |
| Лицензия | Лицензия Apache, версия 2.0 |
| Веб-сайт | ковать |
Инструмент проверки программного обеспечения отложенной абстракции Berkeley ( 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). «Конкурс по верификации программного обеспечения (СВ-КОМП)» (PDF) . Материалы 18-й Международной конференции по средствам и алгоритмам построения и анализа систем . Шпрингер-Верлаг, Гейдельберг.
- ^ Дирк Бейер (2013). «Второй конкурс по верификации программного обеспечения (Итоги SV-COMP 2013)» (PDF) . Материалы 19-й Международной конференции по инструментам и алгоритмам построения и анализа систем . Шпрингер-Верлаг, Гейдельберг.
- ^ Дирк Бейер (2014). «Третий конкурс по верификации программного обеспечения (Итоги SV-COMP 2014)» (PDF) . Материалы 20-й Международной конференции по средствам и алгоритмам построения и анализа систем . Шпрингер-Верлаг, Гейдельберг.
- Примечания
- Павел Швед; Михаил Мандрыкин; Вадим Мутилин (2012). «Анализ предикатов с помощью BLAST 2.7.». Во Фланагане, Кормак; Кениг, Барбара (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 7214. Шпрингер-Верлаг. стр. 525–527. ISBN 978-3-642-28756-5 .
- Бейер, Дирк; Хензингер, Томас А.; Джала, Ранджит; Маджумдар, Рупак (2007). «Взрыв программы проверки моделей программного обеспечения». Международный журнал по программным инструментам для трансфера технологий . 9 (5–6): 505–525. дои : 10.1007/s10009-007-0044-z . S2CID 1662778 .
- Томас А. Хензингер; Ранджит Джала; Рупак Маджумдар и Грегуар Сутре (2003). «Верификация программного обеспечения с помощью Blast». В Болл, Томас и Раджамани, Шрирам К. (ред.). Материалы 10-го семинара SPIN по программному обеспечению для проверки моделей (SPIN 2003) . Конспекты лекций по информатике. Том. 2648. Шпрингер-Верлаг. стр. 235–239. ISBN 3-540-40117-2 .
Внешние ссылки
[ редактировать ] | Эта инструментам программирования, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее . |