The Berkeley Lazy Abstraction Software verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.
Attributes | Values |
---|
rdf:type
| |
rdfs:label
| - BLAST model checker (en)
- BLAST (статический анализатор) (ru)
|
rdfs:comment
| - The Berkeley Lazy Abstraction Software verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision. (en)
- Berkeley Lazy Abstraction Software Verification Tool (BLAST) — программа проверки моделей для языка Си. Задача, решаемая инструментом BLAST — это проверка того, что программа удовлетворяет поведенческим требованиям к ней. BLAST реализует подход абстракция и уточнение по контрпримерам (англ. counterexample-driven automatic abstraction refinement) для конструирования абстрактной модели, которая затем проверяется на свойства безопасности (англ. safety). Абстракция строится по ходу анализа и только до требуемой точности, устанавливаемой в ходе анализа. (ru)
|
foaf:name
| |
name
| |
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
Link from a Wikipage to an external page
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
author
| - Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley (en)
|
developer
| - Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming (en)
|
genre
| |
latest release date
| |
latest release version
| |
license
| |
operating system
| |
programming language
| |
has abstract
| - The Berkeley Lazy Abstraction Software verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision. (en)
- Berkeley Lazy Abstraction Software Verification Tool (BLAST) — программа проверки моделей для языка Си. Задача, решаемая инструментом BLAST — это проверка того, что программа удовлетворяет поведенческим требованиям к ней. BLAST реализует подход абстракция и уточнение по контрпримерам (англ. counterexample-driven automatic abstraction refinement) для конструирования абстрактной модели, которая затем проверяется на свойства безопасности (англ. safety). Абстракция строится по ходу анализа и только до требуемой точности, устанавливаемой в ходе анализа. Оригинальная версия BLAST, разработанная в Беркли, более не поддерживается. В настоящее время BLAST развивается и используется в ИСП РАН.Команда ИСП РАН регулярно участвует с инструментом BLAST в Международных соревнованиях по верификации программного обеспечения (SV-COMP). В 2012 инструмент был награждён золотой медалью в категории DeviceDrivers64 на первых соревнованиях SV-COMP 2012, проводившихся на конференции TACAS 2012 в Таллине. В 2013 году - бронзовой в категории DeviceDrivers64 на вторых соревнованиях SV-COMP 2013, проводившихся на конференции TACAS 2013 в Риме. В 2014 году инструмент был награждён золотой медалью в категории DeviceDrivers64 на третьих соревнованиях SV-COMP 2014, проводившихся на конференции TACAS 2014 в Гренобле. (ru)
|
gold:hypernym
| |
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
latest release date
| |
latest release version
| |
author
| |
developer
| |
genre
| |
license
| |
operating system
| |
programming language
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is Wikipage redirect
of | |