CIVL Release 0.14_1680
Download CIVL-0.14_1680.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.14 of 2014-10-31 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=8 examples/concurrency/adder.cvl
=================== Stats ===================
validCalls : 0
proverCalls : 0
memory (bytes) : 228589568
time (s) : 15.49
maxProcs : 9
statesInstantiated : 46140
statesSaved : 7791
statesSeen : 7775
statesMatched : 1291
steps : 12708
transitions : 9065
The standard properties hold for all executions.
CIVL v0.14 of 2014-10-31 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=7 examples/concurrency/barrier.cvl
17s: mem=302Mb steps=50811 trans=24631 seen=13247 saved=13254 prove=46
32s: mem=240Mb steps=121566 trans=58357 seen=30926 saved=30933 prove=46
47s: mem=226Mb steps=191266 trans=92850 seen=47819 saved=47826 prove=46
62s: mem=258Mb steps=290459 trans=137984 seen=68481 saved=68488 prove=46
77s: mem=245Mb steps=415718 trans=193906 seen=89903 saved=89910 prove=46
92s: mem=300Mb steps=536712 trans=246771 seen=112522 saved=112529 prove=46
107s: mem=377Mb steps=658516 trans=301018 seen=134005 saved=134012 prove=46
122s: mem=377Mb steps=786297 trans=357505 seen=156468 saved=156475 prove=46
137s: mem=377Mb steps=881322 trans=401725 seen=177310 saved=177318 prove=46
152s: mem=409Mb steps=999447 trans=454115 seen=200808 saved=200817 prove=46
=================== Stats ===================
validCalls : 0
proverCalls : 0
memory (bytes) : 428867584
time (s) : 153.52
maxProcs : 8
statesInstantiated : 3148880
statesSaved : 204161
statesSeen : 204149
statesMatched : 256435
steps : 1014095
transitions : 460583
The standard properties hold for all executions.
CIVL v0.14 of 2014-10-31 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=10 -inputW=4 examples/concurrency/blockAdder.cvl
17s: mem=270Mb steps=23559 trans=10732 seen=8228 saved=8248 prove=115
32s: mem=201Mb steps=84980 trans=40261 seen=29973 saved=30035 prove=247
=================== Stats ===================
validCalls : 0
proverCalls : 0
memory (bytes) : 308281344
time (s) : 34.57
maxProcs : 5
statesInstantiated : 368407
statesSaved : 38976
statesSeen : 38898
statesMatched : 14600
steps : 109855
transitions : 53497
The standard properties hold for all executions.
CIVL v0.14 of 2014-10-31 -- http://vsl.cis.udel.edu/civl
verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
17s: mem=316Mb steps=11587 trans=9368 seen=7277 saved=7285 prove=53
32s: mem=172Mb steps=29801 trans=23769 seen=17008 saved=17016 prove=53
47s: mem=241Mb steps=54947 trans=43094 seen=27097 saved=27105 prove=53
62s: mem=254Mb steps=82715 trans=63779 seen=37804 saved=37812 prove=53
77s: mem=177Mb steps=115337 trans=87675 seen=49046 saved=49054 prove=53
92s: mem=348Mb steps=154645 trans=117172 seen=59351 saved=59359 prove=53
107s: mem=378Mb steps=196648 trans=149327 seen=69205 saved=69213 prove=53
122s: mem=377Mb steps=245097 trans=189328 seen=78315 saved=78324 prove=53
137s: mem=378Mb steps=270367 trans=208573 seen=89668 saved=89677 prove=53
152s: mem=378Mb steps=312915 trans=241560 seen=101189 saved=101198 prove=53
=================== Stats ===================
validCalls : 0
proverCalls : 0
memory (bytes) : 396361728
time (s) : 160.26
maxProcs : 10
statesInstantiated : 967463
statesSaved : 109047
statesSeen : 109033
statesMatched : 151316
steps : 337359
transitions : 260348
The standard properties hold for all executions.
CIVL v0.14 of 2014-10-31 -- http://vsl.cis.udel.edu/civl
verify -echo -inputNPROCS_BOUND=5 -inputN_BOUND=3 examples/messagePassing/ring.cvl
=================== Stats ===================
validCalls : 0
proverCalls : 0
memory (bytes) : 109576192
time (s) : 6.3
maxProcs : 6
statesInstantiated : 8758
statesSaved : 817
statesSeen : 665
statesMatched : 0
steps : 1648
transitions : 664
The standard properties hold for all executions.