14.10.2011: Вышла версия 2.7 инструмента верификации BLAST

Центр верификации Linux опубликовал новую версию свободного инструмента верификации BLAST 2.7, который автоматически анализирует Си-программы на предмет нарушения заданных правил корректности посредством реализации метода итеративного уточнения абстракции программы на основе контр-примеров CEGAR.

Версия BLAST 2.7 стала результатом улучшений, внесённых специалистами Центра верификации Linux в BLAST 2.6 в рамках программы Linux Driver Verification , а также в рамках подготовки к Competition on Software Verification, которое состоится в рамках конференции TACAS'12.

Основные улучшения коснулись следующих направлений.

• Ускорении работы
• Реализован быстрый алгоритм анализа алиасов дял указателей на структуры,
  не имеющий ограничений на глубину разыменования.
• Улучшено кеширование запросов постусловий путем добаления их нормализации.
• Ускорено слияние состояний решетки.
• Новые возможности
• Реализована поддержка анализа функциональных указателей (опция -fp),
  для ситуаций когда одна переменная хранит указатель не более чем на одну функцию.
• Обновлен CSIsat, что теперь позволяет анализировать большие целочисленные константы.
• Улучшения в инфраструктуре
• Отделены поддерживаемые опции от неподдерживаемых.
  Вновь добавленные опции включены по умолчанию.
• Регрессионные тесты теперь можно запустить в режиме "соревнований".
• Исправления ошибок
• Исправлен алгоритм O(logN) кеширования useful blocks,
  что позволяет избежать большей части исключений вида FOCIinterface.SAT.

Скачать исходные коды и бинарные сборки для платформы Linux можно из раздела Files сайта проекта. Также смотрите страницу оригинального проекта.