CPAchecker verifier

[Google Scholar] [Wikipedia]

Notes: model checking, BLAST verifier, SV competition
Papers: beyer:cav:2011, necula:cc:2002

CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.
— Wikipedia

BLAST verifier, Software Verification Competition (SV-COMP)

  • CPAchecker: A tool for configurable software verification [beyer:cav:2011]