BLAST (статический анализатор)

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
BLAST
Тип

Инструменты статического анализа

Разработчик

Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley

Операционная система

Linux, Microsoft Windows

Последняя версия

2.5 (11.07.2008)

Лицензия

Apache License, Version 2.0

Сайт

mtc.epfl.ch/software-tools/blast/

Berkeley Lazy Abstraction Software Verification Tool (BLAST) — программа проверки моделей для языка Си. Задача, решаемая инструментом BLAST — это проверка того, что программа удовлетворяет поведенческим требованиям к ней. BLAST реализует подход абстракция и уточнение по контрпримерам (англ. counterexample-driven automatic abstraction refinement) для конструирования абстрактной модели, которая затем проверяется на свойства безопасности (англ. safety). Абстракция строится по ходу анализа и только до требуемой точности, устанавливаемой в ходе анализа.

Литература[править | править вики-текст]

  • Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Software Model Checker Blast. International Journal on Software Tools for Technology Transfer (STTT), 9(5-6):505-525, 2007.
  • Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software Verification with Blast. In Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003), LNCS 2648, Springer-Verlag, pages 235—239, 2003.

См. также[править | править вики-текст]

Ссылки[править | править вики-текст]