CIVL Release 1.3_2459
Download CIVL-1.3_2459.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
>>>>>>>> Adder <<<<<<<<
CIVL v1.3 of 2015-07-23 -- 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.42
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.
>>>>>>>> Barrier <<<<<<<<
CIVL v1.3 of 2015-07-23 -- 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) : 11.0
memory (bytes) : 760217600
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.
>>>>>>>> Block adder <<<<<<<<
CIVL v1.3 of 2015-07-23 -- 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.54
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.
>>>>>>>> Dining philosopher <<<<<<<<
CIVL v1.3 of 2015-07-23 -- 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.65
memory (bytes) : 757596160
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.
>>>>>>>> Adder <<<<<<<<
CIVL v1.3 of 2015-07-23 -- http://vsl.cis.udel.edu/civl
=== Command ===
civl verify -input_NPROCS=4 -inputnsteps=2 -inputnx=2 -inputny=2 -inputNPROCSX=2 -inputNPROCSY=2 -enablePrintf=false ./examples/mpi/diffusion2d.c
=== Stats ===
time (s) : 5.34
memory (bytes) : 367001600
max process count : 5
states : 2995
states saved : 2100
state matches : 0
transitions : 2994
trace steps : 2014
valid calls : 13453
provers : cvc4, z3, cvc3
prover calls : 7
=== Result ===
The standard properties hold for all executions.