PV3 SeaHornchecks assertions in a C program

Application domain/field

Type of tool

Model checker?

Expected input

Program with assertions

Format:

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.

Internals

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

Links

Last commit date

11 January 2021

Related papers

Last publication date

24 November 2018

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.