CIVL Release 0.10_851
Download CIVL-0.10_851.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.10 of 2014-03-28 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputB=8 examples/concurrency/adder.cvl
=================== Stats ===================
validCalls : 19765
proverCalls : 33
memory (bytes) : 1060634624
time (s) : 4.32
maxProcs : 9
statesInstantiated : 46519
statesSaved : 8840
statesSeen : 8824
statesMatched : 1291
steps : 12520
transitions : 10114
The standard properties hold for all executions.
CIVL v0.10 of 2014-03-28 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputB=7 examples/concurrency/barrier.cvl
16s: mem=1068Mb steps=849862 trans=291899 seen=75422 saved=75430 prove=26
=================== Stats ===================
validCalls : 783110
proverCalls : 26
memory (bytes) : 1035468800
time (s) : 17.69
maxProcs : 8
statesInstantiated : 3487402
statesSaved : 89342
statesSeen : 89329
statesMatched : 255919
steps : 1012162
transitions : 345247
The standard properties hold for all executions.
CIVL v0.10 of 2014-03-28 -- 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) : 735576064
time (s) : 3.25
maxProcs : 5
statesInstantiated : 56192
statesSaved : 6162
statesSeen : 6073
statesMatched : 2390
steps : 15900
transitions : 8462
The standard properties hold for all executions.
CIVL v0.10 of 2014-03-28 -- http://vsl.cis.udel.edu/civl
civl verify -echo=true -inputBOUND=9 examples/concurrency/dining.cvl
=================== Stats ===================
validCalls : 979518
proverCalls : 31
memory (bytes) : 1179648000
time (s) : 15.56
maxProcs : 10
statesInstantiated : 967283
statesSaved : 109027
statesSeen : 109011
statesMatched : 151288
steps : 337302
transitions : 260298
The standard properties hold for all executions.
CIVL v0.10 of 2014-03-28 -- 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.73
maxProcs : 6
statesInstantiated : 6216
statesSaved : 940
statesSeen : 767
statesMatched : 0
steps : 1712
transitions : 766
The standard properties hold for all executions.