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

Материал из Seo Wiki - Поисковая Оптимизация и Программирование

Перейти к: навигация, поиск
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.

См. также

Ссылки

Личные инструменты

Served in 0.065 secs.