User Tools

Site Tools



This shows you the differences between two versions of the page.

Link to this comparison view

sv-comp_2015_recursive [2015/01/14 09:28]
ahorn created
sv-comp_2015_recursive [2015/01/14 10:32]
Line 1: Line 1:
 +# 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 
 +# Too few unwindings (only 6) before time out 
sv-comp_2015_recursive.txt · Last modified: 2015/01/14 10:32 by mictau