| dbo: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)
|
| dbo:author
| |
| dbo:developer
| |
| dbo:genre
| |
| dbo:latestReleaseDate
| |
| dbo:latestReleaseVersion
| |
| dbo:license
| |
| dbo:operatingSystem
| |
| dbo:programmingLanguage
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 4833 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:author
|
- Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley (en)
|
| dbp:developer
|
- Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming (en)
|
| dbp:genre
| |
| dbp:latestReleaseDate
| |
| dbp:latestReleaseVersion
| |
| dbp:license
| |
| dbp:name
| |
| dbp:operatingSystem
| |
| dbp:programmingLanguage
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| 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)
|
| rdfs:label
|
- BLAST model checker (en)
- BLAST (статический анализатор) (ru)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| foaf:name
| |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
