[go: up one dir, main page]

An Entity of Type: software, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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.

Property Value
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
  • 2015-10-30 (xsd:date)
dbo:latestReleaseVersion
  • 2.7.3
dbo:license
dbo:operatingSystem
dbo:programmingLanguage
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1044109 (xsd:integer)
dbo:wikiPageLength
  • 4833 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1006121012 (xsd:integer)
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
  • 2015-10-30 (xsd:date)
dbp:latestReleaseVersion
  • 2.700000 (xsd:double)
dbp:license
dbp:name
  • BLAST (en)
dbp:operatingSystem
dbp:programmingLanguage
dbp:wikiPageUsesTemplate
dct: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
  • BLAST (en)
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License