PV3 SeaHornchecks assertions in a C program

Application domain/field

Type of tool

Model checker?

Expected input

Program with assertions


C program, assertions written in the SV-COMP style (e.g., __VERIFIER_error())

Expected output

Result TRUE when the program is safe, Result FALSE when a counterexample was found, or Result UNKNOWN otherwise.


Seahorn is a verification platform that uses Constrained Horn Clauses (CHC) as an intermediate verification language. It focuses on proving safety properties for C programs. It uses software model checking and abstract interpretation techniques.
C CHC Model checking


Related papers

Last publication date

24 November 2018

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.