| Автор (ы) оригинала | Дирк Бейер, Томас Хензингер, Ранджит Джала, Рупак Маджумдар, Беркли |
|---|---|
| Разработчики) | Михаил Мандрыкин, Вадим Мутилин, Павел Швед, Институт системного программирования |
| Стабильный выпуск | 2.7.3 [1] / 30 октября 2015 г . |
| Написано в | OCaml |
| Операционная система | Linux |
| Тип | Статический анализ кода |
| Лицензия | Лицензия Apache, версия 2.0 |
| Веб-сайт | Forge |
Berkeley Ленивый Абстракция Программное обеспечение проверки 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.
- Бейер, Дирк; Henzinger, Thomas A .; Джхала, Ранджит; Маджумдар, Рупак (2007). «Взрыв программы проверки модели». Международный журнал программных средств для передачи технологий . 9 (5–6): 505–525. DOI : 10.1007 / s10009-007-0044-Z . S2CID 1662778 .
- Томас А. Хензингер; Ранджит Джхала; Рупак Маджумдар и Грегуар Сутре (2003). «Проверка программного обеспечения с помощью Blast». В Болл, Томас и Раджамани, Шрирам К. (ред.). Труды 10-го семинара SPIN по программному обеспечению для проверки моделей (SPIN 2003) . Конспект лекций по информатике. 2648 . Springer-Verlag. С. 235–239. ISBN 3-540-40117-2.
Внешние ссылки [ править ]
 | Эта статья о компьютерах - незавершенная . Вы можете помочь Википедии, расширив ее . |
