Commit c84568d7 authored by François Bobot's avatar François Bobot

benchs for frocos paper exported

parent 1d355a49
*.rc
*.avg
*.time
*.csv
\ No newline at end of file
How to reproduce the bench for "Expressing Polymorphic Types in a Many-Sorted Language" of FROCOS'11
The result of this bench can be reproduce using Why3 in the following way:
- You need for that purpose to configure and install why3.
- You need to come back to version acbaa9b711b41e10d3815e3 with
git checkout acbaa9b711b41e10d3815e3, and
- You need to configure and install why3.
- After that you should run why3config and set in ~/.why.conf in the
section [main] the variable "running_provers_max" to your own
number of core.
- Run ./run_bench.sh (it takes 10 hours with 7 core). It creates four files :
partial_deco.csv twin_deco.csv partial_explicit.csv twin_explicit.csv
- Run ./compute_result.sh (it takes 10seconds) to compute the
differences between the four transformations. It needs csvtool.
number of core. You need CVC3, Z3 and Yices.
- Run ./gen_allbench.sh generates one file, bench, by possible set of parameters
- Run ./run_bench.sh (it takes 10 hours with 7 core). It runs the benchs used in the paper
- Run ./compute_result.sh (it takes 10seconds) to compute the comparison tables. It needs csvtool.
nb: bool_inf and unit_inf are used in order to be able to use explicit
\ No newline at end of file
[tools twin_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Twin"
use = "meta.Deco"
[tools partial_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Deco"
[tools twin_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Explicit"
use = "meta.Twin"
[tools partial_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Explicit"
[probs caduceus]
file = "why3/caduceus/abs_why.why"
file = "why3/caduceus/alloca_why.why"
file = "why3/caduceus/alloc_why.why"
file = "why3/caduceus/all_why.why"
file = "why3/caduceus/all_zeros_why.why"
file = "why3/caduceus/arith_why.why"
file = "why3/caduceus/array_why.why"
file = "why3/caduceus/assigns2_why.why"
file = "why3/caduceus/assigns_range_right_why.why"
file = "why3/caduceus/assigns_why.why"
file = "why3/caduceus/band_why.why"
file = "why3/caduceus/binary_search_overflows_why.why"
file = "why3/caduceus/binary_search_safety_why.why"
file = "why3/caduceus/binary_search_why.why"
file = "why3/caduceus/blit_why.why"
file = "why3/caduceus/break_why.why"
file = "why3/caduceus/bresenham_why.why"
file = "why3/caduceus/bug_why.why"
file = "why3/caduceus/calloc_why.why"
file = "why3/caduceus/call_why.why"
file = "why3/caduceus/clash_why.why"
file = "why3/caduceus/consts_why.why"
file = "why3/caduceus/const_why.why"
file = "why3/caduceus/continue_why.why"
file = "why3/caduceus/coord_why.why"
file = "why3/caduceus/copy_why.why"
file = "why3/caduceus/count_bits_2_why.why"
file = "why3/caduceus/count_bits_why.why"
file = "why3/caduceus/dassault_1_why.why"
file = "why3/caduceus/Dillon_why.why"
file = "why3/caduceus/division_why.why"
file = "why3/caduceus/dowhile_why.why"
file = "why3/caduceus/enum_why.why"
file = "why3/caduceus/e_why.why"
file = "why3/caduceus/extern_why.why"
file = "why3/caduceus/fact_why.why"
file = "why3/caduceus/false2_why.why"
file = "why3/caduceus/false_why.why"
file = "why3/caduceus/fib_why.why"
file = "why3/caduceus/flag_checkenum_why.why"
file = "why3/caduceus/flag_why.why"
file = "why3/caduceus/float_why.why"
file = "why3/caduceus/gappa_why.why"
file = "why3/caduceus/ghost2_why.why"
file = "why3/caduceus/ghost_why.why"
file = "why3/caduceus/goto_why.why"
file = "why3/caduceus/heapsort_swap_safety_why.why"
file = "why3/caduceus/heapsort_swap_why.why"
file = "why3/caduceus/heapsort_why.why"
file = "why3/caduceus/heap_why.why"
file = "why3/caduceus/ifs_why.why"
file = "why3/caduceus/incr_why.why"
file = "why3/caduceus/init2_why.why"
file = "why3/caduceus/init_why.why"
file = "why3/caduceus/insertion_safety_why.why"
file = "why3/caduceus/insertion_why.why"
file = "why3/caduceus/invariants_why.why"
file = "why3/caduceus/keiko1_why.why"
file = "why3/caduceus/labels_why.why"
file = "why3/caduceus/latespec_why.why"
file = "why3/caduceus/lexico_why.why"
file = "why3/caduceus/linked-list_why.why"
file = "why3/caduceus/logic_cast_why.why"
file = "why3/caduceus/logic_why.why"
file = "why3/caduceus/loop_assigns_why.why"
file = "why3/caduceus/loop_inv_why.why"
file = "why3/caduceus/loops_why.why"
file = "why3/caduceus/malloc_why.why"
file = "why3/caduceus/math_mod_why.why"
file = "why3/caduceus/matrix_why.why"
file = "why3/caduceus/mean_why.why"
file = "why3/caduceus/muller_why.why"
file = "why3/caduceus/negate_why.why"
file = "why3/caduceus/not_assigns_why.why"
file = "why3/caduceus/null_why.why"
file = "why3/caduceus/overflows_why.why"
file = "why3/caduceus/param_why.why"
file = "why3/caduceus/passing_why.why"
file = "why3/caduceus/pi_again_why.why"
file = "why3/caduceus/pi_why.why"
file = "why3/caduceus/pointer_why.why"
file = "why3/caduceus/purse_why.why"
file = "why3/caduceus/queue_jr_why.why"
file = "why3/caduceus/queue_why.why"
file = "why3/caduceus/rc4_why.why"
file = "why3/caduceus/rec2_why.why"
file = "why3/caduceus/rec_why.why"
file = "why3/caduceus/ref_glob_why.why"
file = "why3/caduceus/ref_why.why"
file = "why3/caduceus/russian_why.why"
file = "why3/caduceus/search_why.why"
file = "why3/caduceus/see_why.why"
file = "why3/caduceus/selection_safety_why.why"
file = "why3/caduceus/selection_why.why"
file = "why3/caduceus/separation1_why.why"
file = "why3/caduceus/separation2_why.why"
file = "why3/caduceus/separation3_why.why"
file = "why3/caduceus/separation4_why.why"
file = "why3/caduceus/separation_why.why"
file = "why3/caduceus/shift_why.why"
file = "why3/caduceus/sort_why.why"
file = "why3/caduceus/sqrt_why.why"
file = "why3/caduceus/strcpy_why.why"
file = "why3/caduceus/string_why.why"
file = "why3/caduceus/struct2_why.why"
file = "why3/caduceus/struct3_why.why"
file = "why3/caduceus/struct4_why.why"
file = "why3/caduceus/struct_why.why"
file = "why3/caduceus/sum1_why.why"
file = "why3/caduceus/sum2_why.why"
file = "why3/caduceus/switch_why.why"
file = "why3/caduceus/tracability_why.why"
file = "why3/caduceus/trop_why.why"
file = "why3/caduceus/unsafe_why.why"
file = "why3/caduceus/zones2_why.why"
file = "why3/caduceus/zones_why.why"
[probs caduceus_why]
file = "why3/caduceus_why/algo64_why.why"
file = "why3/caduceus_why/algo65_why.why"
file = "why3/caduceus_why/all_why.why"
file = "why3/caduceus_why/arith_why.why"
file = "why3/caduceus_why/bresenham_why.why"
file = "why3/caduceus_why/bsearch_why.why"
file = "why3/caduceus_why/dijkstra_why.why"
file = "why3/caduceus_why/exns_why.why"
file = "why3/caduceus_why/fib_why.why"
file = "why3/caduceus_why/find_why.why"
file = "why3/caduceus_why/gcd_why.why"
file = "why3/caduceus_why/heapsort_why.why"
file = "why3/caduceus_why/inductive_why.why"
file = "why3/caduceus_why/loop0_why.why"
file = "why3/caduceus_why/loops_why.why"
file = "why3/caduceus_why/mac_carthy_why.why"
file = "why3/caduceus_why/maximumsort_why.why"
file = "why3/caduceus_why/max_why.why"
file = "why3/caduceus_why/mergesort_why.why"
file = "why3/caduceus_why/oldify_why.why"
file = "why3/caduceus_why/opaque_why.why"
file = "why3/caduceus_why/peano_why.why"
file = "why3/caduceus_why/poly_why.why"
file = "why3/caduceus_why/power_why.why"
file = "why3/caduceus_why/po_why.why"
file = "why3/caduceus_why/queens_why.why"
file = "why3/caduceus_why/quicksort2_why.why"
file = "why3/caduceus_why/quicksort_why.why"
file = "why3/caduceus_why/recfun_why.why"
file = "why3/caduceus_why/return_why.why"
file = "why3/caduceus_why/search_why.why"
file = "why3/caduceus_why/see_why.why"
file = "why3/caduceus_why/selection_why.why"
file = "why3/caduceus_why/set_why.why"
file = "why3/caduceus_why/sqrt_dicho_why.why"
file = "why3/caduceus_why/sqrt_why.why"
file = "why3/caduceus_why/swap0_why.why"
file = "why3/caduceus_why/wpcalls_why.why"
[probs dancing_rev]
file = "why3/dancing/bug2_why.why"
file = "why3/dancing/i_behavior.myset_why.why"
file = "why3/dancing/i_behavior_oracle.myset_why.why"
file = "why3/dancing/i_dancing.myset_why.why"
file = "why3/dancing/i_safety_frame_jessie_why.why"
file = "why3/dancing/i_safety.myset_why.why"
file = "why3/dancing/i_safety.notinft2_why.why"
file = "why3/dancing/i_safety.notinft_why.why"
file = "why3/rev/notinc_disj_FT.ft_is_a_pred_why.why"
file = "why3/rev/notinc_disj_FT.with_notin___why.why"
file = "why3/rev/notinc_disj_FT.without_inductive_FT_why.why"
file = "why3/rev/notin.jessie_frame_why.why"
[bench twin_deco]
tools = twin_deco
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "twin_deco.time"
average = "twin_deco.avg"
csv = "twin_deco.csv"
[bench partial_deco]
tools = partial_deco
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "partial_deco.time"
average = "partial_deco.avg"
csv = "partial_deco.csv"
[bench twin_explicit]
tools = twin_explicit
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "twin_explicit.time"
average = "twin_explicit.avg"
csv = "twin_explicit.csv"
[bench partial_explicit]
tools = partial_explicit
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "partial_explicit.time"
average = "partial_explicit.avg"
csv = "partial_explicit.csv"
[tools twin_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Twin"
use = "meta.Deco"
[tools partial_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Deco"
[tools twin_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Explicit"
use = "meta.Twin"
[tools partial_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Explicit"
[probs caduceus]
file = "why3/caduceus/abs_why.why"
file = "why3/caduceus/alloca_why.why"
file = "why3/caduceus/alloc_why.why"
file = "why3/caduceus/all_why.why"
file = "why3/caduceus/all_zeros_why.why"
file = "why3/caduceus/arith_why.why"
file = "why3/caduceus/array_why.why"
file = "why3/caduceus/assigns2_why.why"
file = "why3/caduceus/assigns_range_right_why.why"
file = "why3/caduceus/assigns_why.why"
file = "why3/caduceus/band_why.why"
file = "why3/caduceus/binary_search_overflows_why.why"
file = "why3/caduceus/binary_search_safety_why.why"
file = "why3/caduceus/binary_search_why.why"
file = "why3/caduceus/blit_why.why"
file = "why3/caduceus/break_why.why"
file = "why3/caduceus/bresenham_why.why"
file = "why3/caduceus/bug_why.why"
file = "why3/caduceus/calloc_why.why"
file = "why3/caduceus/call_why.why"
file = "why3/caduceus/clash_why.why"
file = "why3/caduceus/consts_why.why"
file = "why3/caduceus/const_why.why"
file = "why3/caduceus/continue_why.why"
file = "why3/caduceus/coord_why.why"
file = "why3/caduceus/copy_why.why"
file = "why3/caduceus/count_bits_2_why.why"
file = "why3/caduceus/count_bits_why.why"
file = "why3/caduceus/dassault_1_why.why"
file = "why3/caduceus/Dillon_why.why"
file = "why3/caduceus/division_why.why"
file = "why3/caduceus/dowhile_why.why"
file = "why3/caduceus/enum_why.why"
file = "why3/caduceus/e_why.why"
file = "why3/caduceus/extern_why.why"
file = "why3/caduceus/fact_why.why"
file = "why3/caduceus/false2_why.why"
file = "why3/caduceus/false_why.why"
file = "why3/caduceus/fib_why.why"
file = "why3/caduceus/flag_checkenum_why.why"
file = "why3/caduceus/flag_why.why"
file = "why3/caduceus/float_why.why"
file = "why3/caduceus/gappa_why.why"
file = "why3/caduceus/ghost2_why.why"
file = "why3/caduceus/ghost_why.why"
file = "why3/caduceus/goto_why.why"
file = "why3/caduceus/heapsort_swap_safety_why.why"
file = "why3/caduceus/heapsort_swap_why.why"
file = "why3/caduceus/heapsort_why.why"
file = "why3/caduceus/heap_why.why"
file = "why3/caduceus/ifs_why.why"
file = "why3/caduceus/incr_why.why"
file = "why3/caduceus/init2_why.why"
file = "why3/caduceus/init_why.why"
file = "why3/caduceus/insertion_safety_why.why"
file = "why3/caduceus/insertion_why.why"
file = "why3/caduceus/invariants_why.why"
file = "why3/caduceus/keiko1_why.why"
file = "why3/caduceus/labels_why.why"
file = "why3/caduceus/latespec_why.why"
file = "why3/caduceus/lexico_why.why"
file = "why3/caduceus/linked-list_why.why"
file = "why3/caduceus/logic_cast_why.why"
file = "why3/caduceus/logic_why.why"
file = "why3/caduceus/loop_assigns_why.why"
file = "why3/caduceus/loop_inv_why.why"
file = "why3/caduceus/loops_why.why"
file = "why3/caduceus/malloc_why.why"
file = "why3/caduceus/math_mod_why.why"
file = "why3/caduceus/matrix_why.why"
file = "why3/caduceus/mean_why.why"
file = "why3/caduceus/muller_why.why"
file = "why3/caduceus/negate_why.why"
file = "why3/caduceus/not_assigns_why.why"
file = "why3/caduceus/null_why.why"
file = "why3/caduceus/overflows_why.why"
file = "why3/caduceus/param_why.why"
file = "why3/caduceus/passing_why.why"
file = "why3/caduceus/pi_again_why.why"
file = "why3/caduceus/pi_why.why"
file = "why3/caduceus/pointer_why.why"
file = "why3/caduceus/purse_why.why"
file = "why3/caduceus/queue_jr_why.why"
file = "why3/caduceus/queue_why.why"
file = "why3/caduceus/rc4_why.why"
file = "why3/caduceus/rec2_why.why"
file = "why3/caduceus/rec_why.why"
file = "why3/caduceus/ref_glob_why.why"
file = "why3/caduceus/ref_why.why"
file = "why3/caduceus/russian_why.why"
file = "why3/caduceus/search_why.why"
file = "why3/caduceus/see_why.why"
file = "why3/caduceus/selection_safety_why.why"
file = "why3/caduceus/selection_why.why"
file = "why3/caduceus/separation1_why.why"
file = "why3/caduceus/separation2_why.why"
file = "why3/caduceus/separation3_why.why"
file = "why3/caduceus/separation4_why.why"
file = "why3/caduceus/separation_why.why"
file = "why3/caduceus/shift_why.why"
file = "why3/caduceus/sort_why.why"
file = "why3/caduceus/sqrt_why.why"
file = "why3/caduceus/strcpy_why.why"
file = "why3/caduceus/string_why.why"
file = "why3/caduceus/struct2_why.why"
file = "why3/caduceus/struct3_why.why"
file = "why3/caduceus/struct4_why.why"
file = "why3/caduceus/struct_why.why"
file = "why3/caduceus/sum1_why.why"
file = "why3/caduceus/sum2_why.why"
file = "why3/caduceus/switch_why.why"
file = "why3/caduceus/tracability_why.why"
file = "why3/caduceus/trop_why.why"
file = "why3/caduceus/unsafe_why.why"
file = "why3/caduceus/zones2_why.why"
file = "why3/caduceus/zones_why.why"
[probs caduceus_why]
file = "why3/caduceus_why/algo64_why.why"
file = "why3/caduceus_why/algo65_why.why"
file = "why3/caduceus_why/all_why.why"
file = "why3/caduceus_why/arith_why.why"
file = "why3/caduceus_why/bresenham_why.why"
file = "why3/caduceus_why/bsearch_why.why"
file = "why3/caduceus_why/dijkstra_why.why"
file = "why3/caduceus_why/exns_why.why"
file = "why3/caduceus_why/fib_why.why"
file = "why3/caduceus_why/find_why.why"
file = "why3/caduceus_why/gcd_why.why"
file = "why3/caduceus_why/heapsort_why.why"
file = "why3/caduceus_why/inductive_why.why"
file = "why3/caduceus_why/loop0_why.why"
file = "why3/caduceus_why/loops_why.why"
file = "why3/caduceus_why/mac_carthy_why.why"
file = "why3/caduceus_why/maximumsort_why.why"
file = "why3/caduceus_why/max_why.why"
file = "why3/caduceus_why/mergesort_why.why"
file = "why3/caduceus_why/oldify_why.why"
file = "why3/caduceus_why/opaque_why.why"
file = "why3/caduceus_why/peano_why.why"
file = "why3/caduceus_why/poly_why.why"
file = "why3/caduceus_why/power_why.why"
file = "why3/caduceus_why/po_why.why"
file = "why3/caduceus_why/queens_why.why"
file = "why3/caduceus_why/quicksort2_why.why"
file = "why3/caduceus_why/quicksort_why.why"
file = "why3/caduceus_why/recfun_why.why"
file = "why3/caduceus_why/return_why.why"
file = "why3/caduceus_why/search_why.why"
file = "why3/caduceus_why/see_why.why"
file = "why3/caduceus_why/selection_why.why"
file = "why3/caduceus_why/set_why.why"
file = "why3/caduceus_why/sqrt_dicho_why.why"
file = "why3/caduceus_why/sqrt_why.why"
file = "why3/caduceus_why/swap0_why.why"
file = "why3/caduceus_why/wpcalls_why.why"
[probs dancing_rev]
file = "why3/dancing/bug2_why.why"
file = "why3/dancing/i_behavior.myset_why.why"
file = "why3/dancing/i_behavior_oracle.myset_why.why"
file = "why3/dancing/i_dancing.myset_why.why"
file = "why3/dancing/i_safety_frame_jessie_why.why"
file = "why3/dancing/i_safety.myset_why.why"
file = "why3/dancing/i_safety.notinft2_why.why"
file = "why3/dancing/i_safety.notinft_why.why"
file = "why3/rev/notinc_disj_FT.ft_is_a_pred_why.why"
file = "why3/rev/notinc_disj_FT.with_notin___why.why"
file = "why3/rev/notinc_disj_FT.without_inductive_FT_why.why"
file = "why3/rev/notin.jessie_frame_why.why"
[bench partial_deco]
tools = partial_deco
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "partial_deco.time"
average = "partial_deco.avg"
csv = "partial_deco.csv"
[tools twin_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Twin"
use = "meta.Deco"
[tools partial_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Deco"
[tools twin_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Explicit"
use = "meta.Twin"
[tools partial_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Explicit"
[probs caduceus]
file = "why3/caduceus/abs_why.why"
file = "why3/caduceus/alloca_why.why"
file = "why3/caduceus/alloc_why.why"
file = "why3/caduceus/all_why.why"
file = "why3/caduceus/all_zeros_why.why"
file = "why3/caduceus/arith_why.why"
file = "why3/caduceus/array_why.why"
file = "why3/caduceus/assigns2_why.why"
file = "why3/caduceus/assigns_range_right_why.why"
file = "why3/caduceus/assigns_why.why"
file = "why3/caduceus/band_why.why"
file = "why3/caduceus/binary_search_overflows_why.why"
file = "why3/caduceus/binary_search_safety_why.why"
file = "why3/caduceus/binary_search_why.why"
file = "why3/caduceus/blit_why.why"
file = "why3/caduceus/break_why.why"
file = "why3/caduceus/bresenham_why.why"
file = "why3/caduceus/bug_why.why"
file = "why3/caduceus/calloc_why.why"
file = "why3/caduceus/call_why.why"
file = "why3/caduceus/clash_why.why"
file = "why3/caduceus/consts_why.why"
file = "why3/caduceus/const_why.why"
file = "why3/caduceus/continue_why.why"
file = "why3/caduceus/coord_why.why"
file = "why3/caduceus/copy_why.why"
file = "why3/caduceus/count_bits_2_why.why"
file = "why3/caduceus/count_bits_why.why"
file = "why3/caduceus/dassault_1_why.why"
file = "why3/caduceus/Dillon_why.why"
file = "why3/caduceus/division_why.why"
file = "why3/caduceus/dowhile_why.why"
file = "why3/caduceus/enum_why.why"
file = "why3/caduceus/e_why.why"
file = "why3/caduceus/extern_why.why"
file = "why3/caduceus/fact_why.why"
file = "why3/caduceus/false2_why.why"
file = "why3/caduceus/false_why.why"
file = "why3/caduceus/fib_why.why"
file = "why3/caduceus/flag_checkenum_why.why"