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.

Notes related to SeaHorn verifier

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

Papers related to SeaHorn verifier

• Executable counterexamples in software model checking [gennari:vstte:2018]
• The SeaHorn verification framework [gurfinkel:cav:2015]