CIVL Release 0.16_1811
Download CIVL-0.16_1811.tgz, unpack, and follow
the instructions in the README file. You may also
refer to the CIVL manual for more
details about CIVL.
Benchmark Results
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=8 examples/concurrency/adder.cvl
=================== Stats ===================
validCalls : 67650
proverCalls : 60
memory (bytes) : 180879360
time (s) : 6.62
maxProcs : 9
statesInstantiated : 46140
statesSaved : 7791
statesSeen : 7775
statesMatched : 1291
steps : 12708
transitions : 9065
The standard properties hold for all executions.
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=7 examples/concurrency/barrier.cvl
17s: mem=346Mb steps=123789 trans=57022 seen=28924 saved=28936 prove=46
32s: mem=250Mb steps=289793 trans=133083 seen=65189 saved=65202 prove=46
47s: mem=185Mb steps=412466 trans=193456 seen=95298 saved=95311 prove=46
62s: mem=379Mb steps=601806 trans=278150 seen=131283 saved=131296 prove=46
77s: mem=379Mb steps=807130 trans=369110 seen=167701 saved=167714 prove=46
92s: mem=378Mb steps=1010004 trans=458913 seen=203766 saved=203779 prove=46
=================== Stats ===================
validCalls : 2968626
proverCalls : 46
memory (bytes) : 396361728
time (s) : 91.63
maxProcs : 8
statesInstantiated : 3143338
statesSaved : 204029
statesSeen : 204017
statesMatched : 255919
steps : 1012162
transitions : 459935
The standard properties hold for all executions.
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=10 -inputW=4 examples/concurrency/blockAdder.cvl
=================== Stats ===================
validCalls : 30039
proverCalls : 291
memory (bytes) : 311427072
time (s) : 9.4
maxProcs : 5
statesInstantiated : 54022
statesSaved : 6951
statesSeen : 6873
statesMatched : 2390
steps : 15220
transitions : 9262
The standard properties hold for all executions.
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
17s: mem=318Mb steps=38139 trans=29562 seen=15338 saved=15352 prove=53
32s: mem=190Mb steps=96327 trans=74295 seen=33396 saved=33411 prove=53
47s: mem=296Mb steps=127619 trans=99092 seen=50333 saved=50348 prove=53
62s: mem=368Mb steps=168931 trans=130568 seen=66645 saved=66660 prove=53
77s: mem=374Mb steps=221414 trans=168946 seen=84439 saved=84454 prove=53
92s: mem=375Mb steps=293230 trans=223786 seen=101460 saved=101474 prove=53
=================== Stats ===================
validCalls : 4134543
proverCalls : 53
memory (bytes) : 393216000
time (s) : 98.64
maxProcs : 10
statesInstantiated : 967316
statesSaved : 109033
statesSeen : 109019
statesMatched : 151288
steps : 337310
transitions : 260306
The standard properties hold for all executions.
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
verify -echo -inputNPROCS_BOUND=10 -inputN_BOUND=3 examples/concurrency/ring.cvl
=================== Stats ===================
validCalls : 13552
proverCalls : 297
memory (bytes) : 182976512
time (s) : 9.71
maxProcs : 11
statesInstantiated : 38794
statesSaved : 3272
statesSeen : 2675
statesMatched : 0
steps : 6968
transitions : 2674
The standard properties hold for all executions.