CIVL Release 0.11_930
Download CIVL-0.11_930.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.11 of 2014-04-22 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputB=8 examples/concurrency/adder.cvl
=================== Stats ===================
validCalls : 19765
proverCalls : 33
memory (bytes) : 1056440320
time (s) : 5.08
maxProcs : 9
statesInstantiated : 46519
statesSaved : 8840
statesSeen : 8824
statesMatched : 1291
steps : 12520
transitions : 10114
The standard properties hold for all executions.
CIVL v0.11 of 2014-04-22 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputB=7 examples/concurrency/barrier.cvl
16s: mem=615Mb steps=670396 trans=229599 seen=60013 saved=60020 prove=26
=================== Stats ===================
validCalls : 783110
proverCalls : 26
memory (bytes) : 422576128
time (s) : 21.01
maxProcs : 8
statesInstantiated : 3487402
statesSaved : 89342
statesSeen : 89329
statesMatched : 255919
steps : 1012162
transitions : 345247
The standard properties hold for all executions.
CIVL v0.11 of 2014-04-22 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputB=10 -inputW=4 examples/concurrency/blockAdder.cvl
=================== Stats ===================
validCalls : 12464
proverCalls : 152
memory (bytes) : 734003200
time (s) : 3.51
maxProcs : 5
statesInstantiated : 56192
statesSaved : 6162
statesSeen : 6073
statesMatched : 2390
steps : 15900
transitions : 8462
The standard properties hold for all executions.
CIVL v0.11 of 2014-04-22 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputBOUND=9 examples/concurrency/dining.cvl
16s: mem=1172Mb steps=297651 trans=229099 seen=97002 saved=97012 prove=31
=================== Stats ===================
validCalls : 1197314
proverCalls : 31
memory (bytes) : 1134034944
time (s) : 17.02
maxProcs : 10
statesInstantiated : 967315
statesSaved : 109035
statesSeen : 109019
statesMatched : 151288
steps : 337310
transitions : 260306
The standard properties hold for all executions.
CIVL v0.11 of 2014-04-22 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputNPROCS_BOUND=5 -inputN_BOUND=3 examples/messagePassing/ring.cvl
=================== Stats ===================
validCalls : 2431
proverCalls : 112
memory (bytes) : 257425408
time (s) : 1.86
maxProcs : 6
statesInstantiated : 6216
statesSaved : 940
statesSeen : 767
statesMatched : 0
steps : 1712
transitions : 766
The standard properties hold for all executions.