PV3 ⊧ SeaHornchecks assertions in a C program

Application domain/field

• Safety properties
• Software model checking
• Abstract interpretation
• Software verification

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.