User Tools

Site Tools


sv-comp_2015_recursive
# For Arrays, BitVectors, ControlFlowInteger/loop-acceleration:
# time cbmc --verbosity 10 with increasing unwinding bounds to figure out
# whether memory or CPU time is the main limiting factor; then use gprof (CPU
# time) or valgrind/massif (memory) to identify the key bits requiring
# improvement

# Too few unwindings (only 12) before time out
Recursive/recursive/Addition03_false-unreach-call.c
# Too few unwindings (only 6) before time out
Recursive/recursive/Fibonacci05_false-unreach-call_true-termination.c
sv-comp_2015_recursive.txt · Last modified: 2015/01/14 10:32 by mictau