CIVL Release 1.0_2265
Download CIVL-1.0_2265.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 v1.0 of 2015-04-18 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=8 examples/concurrency/adder.cvl
=== Command ===
civl verify -echo -inputB=8 examples/concurrency/adder.cvl
=== Stats ===
time (s) : 6.43
memory (bytes) : 181403648
max process count : 9
states : 9589
states saved : 7755
state matches : 1291
transitions : 10879
trace steps : 9029
valid calls : 79426
provers : cvc4, z3, cvc3
prover calls : 33
=== Result ===
The standard properties hold for all executions.
CIVL v1.0 of 2015-04-18 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=7 examples/concurrency/barrier.cvl
17s: mem=354Mb trans=340862 traceSteps=158177 explored=257759 saved=75086 prove=25
32s: mem=372Mb trans=722507 traceSteps=340355 explored=544572 saved=162432 prove=25
47s: mem=416Mb trans=1231590 traceSteps=566530 explored=916425 saved=251378 prove=25
=== Command ===
civl verify -echo -inputB=7 examples/concurrency/barrier.cvl
=== Stats ===
time (s) : 49.6
memory (bytes) : 432537600
max process count : 8
states : 999760
states saved : 270186
state matches : 349567
transitions : 1349326
trace steps : 619740
valid calls : 1279865
provers : cvc4, z3, cvc3
prover calls : 25
=== Result ===
The standard properties hold for all executions.
CIVL v1.0 of 2015-04-18 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=10 -inputW=4 examples/concurrency/blockAdder.cvl
=== Command ===
civl verify -echo -inputB=10 -inputW=4 examples/concurrency/blockAdder.cvl
=== Stats ===
time (s) : 5.08
memory (bytes) : 109576192
max process count : 5
states : 3911
states saved : 2333
state matches : 230
transitions : 4140
trace steps : 2484
valid calls : 14022
provers : cvc4, z3, cvc3
prover calls : 51
=== Result ===
The standard properties hold for all executions.
CIVL v1.0 of 2015-04-18 -- http://vsl.cis.udel.edu/civl
verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
17s: mem=353Mb trans=115320 traceSteps=89562 explored=70099 saved=44355 prove=29
32s: mem=375Mb trans=278039 traceSteps=211893 explored=164398 saved=98266 prove=29
=== Command ===
civl verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
=== Stats ===
time (s) : 34.97
memory (bytes) : 394788864
max process count : 10
states : 186023
states saved : 109078
state matches : 151288
transitions : 337310
trace steps : 260351
valid calls : 1191870
provers : cvc4, z3, cvc3
prover calls : 29
=== Result ===
The standard properties hold for all executions.
CIVL v1.0 of 2015-04-18 -- http://vsl.cis.udel.edu/civl
verify -echo -inputNPROCS_BOUND=10 -inputN_BOUND=3 examples/concurrency/ring.cvl
=== Command ===
civl verify -echo -inputNPROCS_BOUND=10 -inputN_BOUND=3 examples/concurrency/ring.cvl
=== Stats ===
time (s) : 7.68
memory (bytes) : 182976512
max process count : 11
states : 6880
states saved : 4574
state matches : 0
transitions : 6879
trace steps : 3986
valid calls : 14758
provers : cvc4, z3, cvc3
prover calls : 38
=== Result ===
The standard properties hold for all executions.