Русская Википедия:BLAST (статический анализатор)
Berkeley Lazy Abstraction Software Verification Tool (BLAST) — программа проверки моделей для языка Си. Задача, решаемая инструментом BLAST — это проверка того, что программа удовлетворяет поведенческим требованиям к ней. BLAST реализует подход абстракция и уточнение по контрпримерам (Шаблон:Lang-en) для конструирования абстрактной модели, которая затем проверяется на свойства безопасности (Шаблон:Lang-en). Абстракция строится по ходу анализа и только до требуемой точности, устанавливаемой в ходе анализа.
Оригинальная версия BLAST[1], разработанная в Беркли, более не поддерживается. В настоящее время BLAST развивается и используется в ИСП РАН. Команда ИСП РАН регулярно участвует с инструментом BLAST в Международных соревнованиях по верификации программного обеспечения (SV-COMP).
В 2012 инструмент был награждён золотой медалью в категории DeviceDrivers64 на первых соревнованиях SV-COMP 2012, проводившихся на конференции TACAS 2012 в Таллине. [2]
В 2013 году - бронзовой в категории DeviceDrivers64 на вторых соревнованиях SV-COMP 2013, проводившихся на конференции TACAS 2013 в Риме. [3]
В 2014 году инструмент был награждён золотой медалью в категории DeviceDrivers64 на третьих соревнованиях SV-COMP 2014, проводившихся на конференции TACAS 2014 в Гренобле. [4]
Литература
См. также
Примечания
Ссылки
