Software verification with BLAST

摘要: Blast (the Berkeley Lazy Abstraction Software verification Tool) is a system for checking safety properties of C programs using automatic property-driven construction and model software abstractions. implements an abstract-model check-refine loop to check reachability specified label in the program. The abstract built on fly predicate abstraction. This then checked reachability. If there no (abstract) path error label, reports that safe produces succinct proof. Otherwise, it checks if feasible symbolic execution feasible, outputs as trace, otherwise, uses infeasibility refine model. short-circuits from abstraction refinement, integrating three steps tightly through “lazy abstraction” [5]. integration can offer significant advantages performance by avoiding repetition work one iteration next.