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

BLAST
Тип	Инструменты статического анализа
Разработчик	Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
ОС	GNU/Linux, Microsoft Windows
Версия	2.5 (11.07.2008)
Лицензия	Apache License, Version 2.0
Сайт	BLAST Project

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.

См. также

• Статический анализ кода

Ссылки

• Сайт BLAST