BLAST verifier

[Google Scholar] [Wikipedia]

Notes: model checking, CPAchecker verifier, extended static checking, AoRTE, SV competition, CEGAR
Papers: beyer:sas:2004, beyer:ijsttt:2007, necula:cc:2002

BLAST (Berkeley Lazy Abstraction Software verification Tool) was an early C program verification tool.

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.
— Wikipedia

CPAchecker verifier, Software Verification Competition (SV-COMP)