CIVL Release 1.2_2429
Download CIVL-1.2_2429.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.2 of 2015-07-13 -- 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) : 2.24
memory (bytes) : 220725248
max process count : 9
states : 9589
states saved : 7754
state matches : 1291
transitions : 10879
trace steps : 9028
valid calls : 79426
provers : cvc4, z3, cvc3
prover calls : 33
=== Result ===
The standard properties hold for all executions.
CIVL v1.2 of 2015-07-13 -- http://vsl.cis.udel.edu/civl
verify -echo -inputB=7 examples/concurrency/barrier.cvl
=== Command ===
civl verify -echo -inputB=7 examples/concurrency/barrier.cvl
=== Stats ===
time (s) : 10.7
memory (bytes) : 759693312
max process count : 8
states : 999752
states saved : 269508
state matches : 349567
transitions : 1349318
trace steps : 619062
valid calls : 3924258
provers : cvc4, z3, cvc3
prover calls : 25
=== Result ===
The standard properties hold for all executions.
CIVL v1.2 of 2015-07-13 -- 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) : 1.44
memory (bytes) : 155713536
max process count : 5
states : 3911
states saved : 1873
state matches : 230
transitions : 4140
trace steps : 2024
valid calls : 13882
provers : cvc4, z3, cvc3
prover calls : 51
=== Result ===
The standard properties hold for all executions.
CIVL v1.2 of 2015-07-13 -- http://vsl.cis.udel.edu/civl
verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
=== Command ===
civl verify -echo -inputBOUND=9 examples/concurrency/dining.cvl
=== Stats ===
time (s) : 8.55
memory (bytes) : 757071872
max process count : 10
states : 186013
states saved : 109071
state matches : 151288
transitions : 337300
trace steps : 260344
valid calls : 4210161
provers : cvc4, z3, cvc3
prover calls : 29
=== Result ===
The standard properties hold for all executions.
CIVL v1.2 of 2015-07-13 -- 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) : 2.38
memory (bytes) : 220725248
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.