This page is the submission of SeaHorn -- a software verification tool to the 2015 Competition on Software Verification SVCOMP.

#Team * Arie Gurfinkel (SEI / CMU) * Temesghen Kahsai (NASA Ames / CMU) * Jorge A. Navas (NASA Ames / SGT)

Tool

• Download: here

Installation

• Untar: tar jxf seahorn-svcomp15.tar.bz2

Run

  python PATH_TO_SEAHORN/bin/seahorn-svcomp-par.py [OPTIONS] file

Options

• -m64 sets int to 32 bits and long and pointer types to 64 bits.
• --cex=CEX CEX is the location where to store the counter-example.
• --spec=SPEC SPEC is the property file.

Categories

• SeaHorn is participating in all categories.
• All categories except for DeviceDrivers64 do not require any options.
• DeviceDrivers64 requires -m64

Results

Output contains the string:

• Result TRUE when the program is safe
• Result FALSE when a counterexample is found.
• Result UNKNOWN otherwise.