1. Teme Kahsai
  2. SeaHorn

Wiki

Clone wiki

SeaHorn / Home

Screen Shot 2014-10-30 at 11.40.43 PM.png

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

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.

Updated