WikiDer > Проверка моделей BLAST

BLAST model checker
ВЗРЫВ
Оригинальный автор (ы)Дирк Бейер, Томас Хензингер, Ранджит Джала, Рупак Маджумдар, Беркли
Разработчики)Михаил Мандрыкин, Вадим Мутилин, Павел Швед, Институт системного программирования
Стабильный выпуск
2.7.3[1] / 18 ноября 2014 г.; 6 лет назад (2014-11-18)
Написано вOCaml
Операционная системаLinux
ТипСтатический анализ кода
ЛицензияЛицензия Apache, версия 2.0
Интернет сайтковать.ispras.RU/ проекты/взрыв

В Инструмент проверки программного обеспечения Berkeley Lazy Abstraction (ВЗРЫВ) это программного обеспечения проверка модели инструмент для C программы. BLAST решает задачу проверить, удовлетворяет ли программное обеспечение поведенческим требованиям связанных с ним интерфейсов. BLAST нанимает контрпример-приводимое автоматическое уточнение абстракции для построения абстрактной модели, которая затем проверяется моделью на свойства безопасности. Абстракция построена на лету, и только запрошенному точность.

Достижения

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

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

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

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

  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, Гейдельберг.
Примечания
  • Павел Швед; Михаил Мандрыкин; Вадим Мутилин (2012). «Анализ предикатов с помощью BLAST 2.7.». Во Фланагане, Кормаке; Кениг, Барбара (ред.). Инструменты и алгоритмы построения и анализа систем. Конспект лекций по информатике. 7214. Springer-Verlag. С. 525–527. ISBN 978-3-642-28756-5.
  • Бейер, Дирк; Henzinger, Thomas A .; Джала, Ранджит; Маджумдар, Рупак (2007). «Взрыв программы проверки модели». Международный журнал программных средств для передачи технологий. 9 (5–6): 505–525. Дои:10.1007 / s10009-007-0044-z.
  • Томас А. Хензингер; Ранджит Джхала; Рупак Маджумдар и Грегуар Сутре (2003). «Проверка программного обеспечения с помощью Blast». В Болл, Томас и Раджамани, Шрирам К. (ред.). Труды 10-го семинара SPIN по программному обеспечению для проверки моделей (SPIN 2003). Конспект лекций по информатике. 2648. Springer-Verlag. С. 235–239. ISBN 3-540-40117-2.

внешняя ссылка