User Tools

Site Tools


sv-comp_2015_control-flow-integer

Michael says: no known issues here.

Ruben: Current trunk version is able to solve all programs without any bugs.

SV-COMP'15 (programs where cbmc gave wrong/unknown answer):

unknown: ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c
trunk version: finds a cex in 0.2 secs. The cex is verified in 5 secs by the witness checker.
unknown: ssh-simplified/s3_srvr_10_false-unreach-call.cil.c
trunk version: finds a cex in 0.2 secs. The cex is verified in 2 secs by the witness checker.
true: ssh-simplified/s3_srvr_2_false-unreach-call.cil.c
trunk version: finds a cex in 4 secs. The cex is verified in 5 secs by the witness checker.
witness timeout: locks/test_locks_15_false-unreach-call.c
trunk version: finds a cex in 0.2 secs. The witness checkers times out.

The cex has 63 states. If --beautify is used then the cex has 62 states.
Minimising the cex may improve the performance of the witness checker.

For example, ESBMC returns a cex with 48 states which is verified by the witness checker in 2 min 27 secs.

For using the witness checker do the following steps:

1. Download CPAchecker at: http://cpachecker.sosy-lab.org/CPAchecker-1.4-unix.tar.bz2
2. In the CPAchecker directory do the following command: 
   scripts/cpa.sh -witness-check -spec <witness> -spec <propertyfile> <program> 

3. Alternatively, you can use the following 'witness.sh' bash script:

#!/bin/bash

if [ "x$1" = "x" ]; then
  echo "USAGE: ./witness.sh <property-file> <program> <witness>"
  exit 1
fi

Note: CPAchecker Requires Java 1.7 to work.
sv-comp_2015_control-flow-integer.txt · Last modified: 2015/01/14 14:21 by ruben