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

Опубликовано admin в Пнд, 23/01/2012 - 08:29

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

Версия BLAST 2.6 стала результатом улучшений, внесённых специалистами Центра верификации Linux в рамках программы Linux Driver Verification в версию BLAST 2.5, которая была разработана командой европейских и американских учёных и развитие которой приостановилось в середине 2008 года.

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

  • Ускорении работы
    • Общее ускорение анализа в 8 раз для маленьких программ и в 30 раз для программ среднего размера
    • Реализация логарифмического алгоритма useful-blocks для ускорения анализа трассы
    • Улучшенная интеграция с SMT солверами
      • эффективная конкатенация строк
      • кеширование конвертированных формул
      • оптимизация опций CVC3 для типовых задач BLAST
    • Нормализация формул передана солверам, где это реализовано более эффективно(опция -skipnorm)
    • Ускорение анализа алиасов
      • must-алиасы обрабатываются независимо и быстрее, чем may-алиасы (опция -nomusts)
      • удалена отладочная печать из основных циклов, где даже проверка флага debug занимала в совокупности значительное время
    • Настройка виртуальной машины OCaml для эффективной работы инструмента BLAST (скрипт "ocamltune")
  • Исправления существенных ошибок

    • Исправление некорректного анализа при включённой опции использования решёток (опции -stop-sep и -merge). (За счет этого время анализа возросло в 1.5 раза, но исчезли ошибки, приводящие к ненахождению ошибок в анализируемой программе). См. проблему #330

    • Кастирование bool-to-int при вызове функций. См. проблему #334
  • Парсер
    • Обновлён парсер (CIL), исправлен ряд ошибок (см. опции -ignoredupfn и -nosserr)
    • Некоторые несущественные ошибки сделаны предупреждениями
  • Новые возможности
    • Реализованы опции ограничения глубины анализируемого стека вызовов (см. опции -fdepth, -important-attrs и -inline-attrs)
    • Интерпретация константных указателей как must-алиасов (см. опцию -const)
  • Улучшения в инфраструктуре
    • Улучшен набор регрессионных тестов
    • Удалены несвободные компоненты (солвер simplify заменен на CVC3, удалены неиспользуемые Vampyre, FOCI и CLPprover)

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