- BLAST (статический анализатор)
-
BLAST Тип Разработчик Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
Операционная система Последняя версия 2.5 (11.07.2008)
Лицензия Сайт 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.
См. также
Ссылки
Категории:- Программное обеспечение по алфавиту
- Формальные методы
- Исследование программ
- Статические анализаторы кода
Wikimedia Foundation. 2010.