SeaHorn verifier

SeaHorn verifier
[Google Scholar] [Website]

Notes: LLVM compiler, abstract interpretation
Papers: gurfinkel:cav:2015

SeaHorn is a framework and tool for verification of safety properties in C programs. It uses the LLVM compiler as a frontend and verification is based on abstract interpretation, constrained Horn clauses and PDR/IC3 based model checking.

Extended static checking (ESC), Software Verification Competition (SV-COMP)