This page is the submission of the FrankenBit bit-precise software verifier to the 2014 Competition on Software Verification (SV-COMP).

Team

Arie Gurfinkel and Anton Belov

Tool

Download: https://bitbucket.org/arieg/fbit/downloads/fbit-svcomp14.tar.gz

Requirements

• Multiprecision arithmetic library (C++ bindings). sudo apt-get install libgmpxx4ldbl

Installation

• Untar: tar xvzf fbit-svcomp14.tar.gz

Run

  PATH_TO_FBIT/bin/fbit.py [OPTIONS] file

Options

• -m64 sets int to 32 bits and long and pointer types to 64 bits
• --cex=FILE enables counter-example generation to FILE
• --spec=FILE reads specification property from FILE

Categories

• FrankenBit is participating in categories ControlFlowIntegers, Simple, ProductLines, DeviceDrivers64.
• 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 and the string Result FALSE when a counterexample is found.

Contact

For additional information please contact Arie Gurfinkel (arie at cmu dot edu) or Anton Belov (anton dot belov at ucd dot ie)