User Tools

Site Tools


sv-comp_2015

What You Need To Do

For your category (see below), look at the information provided on the sub-page (list of known failures with preliminary diagnosis by Michael) and possibly the results on:

http://sv-comp.sosy-lab.org/2015/results/META_Overall.table.html

and for all of the benchmark that do not have a green result or where CBMC is slower than ESBMC, work out which of the categories it is in and do the following:

  1. Bugs : benchmarks where CBMC crashes or produces and incorrect answer. For these we need reduced test cases to add to the regression suite; be aware that there was a bug in the graphml counterexample code that caused a crash of CBMC (indeed in fairly random ways) - this has been fixed in trunk; thus do check the sub-page whether the example is also listed there.
  2. Missing features : benchmarks where we cannot give the correct answer because CBMC lacks one or more key features (for example, loop acceleration would be needed or that we can't perform the relevant kind of analysis). For these we need a concise summary of the feature that is needed.
  3. Performance problems : benchmarks where CBMC runs out of time or memory before getting a result. For this we need a measure of how much time or memory was used and which is the bottleneck. Ideally we need to know where in CBMC the bottleneck is. Does slicing fix it?
  4. Incorrect benchmarks : benchmarks that have been incorrectly classified. For this we need a good argument, citing the appropriate standards, and an executable test case that shows why the benchmark is wrong.

Add these to the relevant page below.

For performance problems, you may wish to record the CPU time and memory consumption over a sequence of increasing unwindings to understand which of them is the main bit to be tackled. Then consult profiling and/or ask Michael/Martin about memory profiling.

To turn all of or parts of the SV-COMP benchmarks into regression tests as found in the CBMC SVN, consult the sv-comp-utilities page.

Arrays

BitVectors

Concurrency

ControlFlow

ControlFlowInteger

ECA

Loops

ProductLines

DeviceDrivers64

Floats

HeapManipulation

MemorySafety

Recursive

Sequentialized

Simple

Termination

Overall

sv-comp_2015.txt · Last modified: 2015/01/14 16:44 by mbrain