BLAST model checker

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
BLAST
Original authorsDirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
DevelopersMikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming
Stable release
2.7.3[1] / 30 October 2015; 10 years ago (2015-10-30)
Repository
  • {{URL|example.com|optional display text}}Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
Written inOCaml
Engine
    Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
    Operating systemLinux
    TypeStatic code analysis
    LicenseApache License, Version 2.0
    Websiteforge.ispras.ru/projects/blast

    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.

    Achievements

    [edit | edit source]

    BLAST came first in the category DeviceDrivers64 in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.[2]

    BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.[3]

    BLAST came first in the category DeviceDrivers64 in the 3rd Competition on Software Verification (2014), that was held at TACAS 2014 in Grenoble.[4]

    References

    [edit | edit source]
    1. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    2. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    3. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    4. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    Notes
    • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    [edit | edit source]


    Stub icon

    This programming-tool-related article is a stub. You can help Wikipedia by expanding it.

    Retrieved from "http://70.231.62.181/index.php?title=BLAST_model_checker&oldid=2889896"