(Created page with '{{DISPLAYTITLE:Benchmarks for the ProB (Dis)prover}}') |
(Update links) |
||
| (6 intermediate revisions by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{DISPLAYTITLE:Benchmarks for the ProB (Dis)prover}} | {{DISPLAYTITLE:Benchmarks for the ProB (Dis)prover}} | ||
[[Category:ProB Disprover]] | |||
We benchmarked the ProB disprove for an article currently under consideration for SEFM 2015. | |||
== Raw Data == | |||
All raw data is available as csv files from [https://www3.hhu.de/stups/models/sefm2015_disprover/raw/ here]. | |||
A zip file containing all csv files is available [https://www3.hhu.de/stups/models/sefm2015_disprover/raw/rawdata.zip here]. | |||
== Data Visualisations == | |||
Due to the page limit, we could not give all the diagrams and visualisation of the benchmark results in the article. | |||
They are available here: | |||
=== Landing Gears === | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_provers_only.pdf Su and Abrial, Landing Gear Model 1, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_tactic.pdf Su and Abrial, Landing Gear Model 1, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_provers_only.pdf Su and Abrial, Landing Gear Model 2, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_tactic.pdf Su and Abrial, Landing Gear Model 2, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_provers_only.pdf Su and Abrial, Landing Gear Model 3, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_tactic.pdf Su and Abrial, Landing Gear Model 3, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_provers_only.pdf Hansen et. al., Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_tactic.pdf Hansen et. al., Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_provers_only.pdf Mammar and Laleau, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_tactic.pdf Mammar and Laleau, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_provers_only.pdf André, Attiogbé and Lanoix, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_tactic.pdf André, Attiogbé and Lanoix, Tactics] | |||
=== Further Models === | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_provers_only.pdf Colley, Canbus, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_tactic.pdf Colley, Canbus, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf Andriamiarina and Méry, Graphcoloring, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf Andriamiarina and Méry, Graphcoloring, Tactics] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf Wiegard, Stuttgart 21, Provers alone] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf Wiegard, Stuttgart 21, Tactics] | |||
=== Summaries === | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_landiggears.pdf Tactics on Landing Gears] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_all_models.pdf Tactics on all Models] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_landiggears.pdf Provers alone on Landing Gears] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_all_models.pdf Provers alone on all Models] | |||
=== Surplus of ProB === | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus.pdf Surplus of ProB (added last)] | |||
* [https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus2.pdf Surplus of ProB (added first)] | |||
We benchmarked the ProB disprove for an article currently under consideration for SEFM 2015.
All raw data is available as csv files from here. A zip file containing all csv files is available here.
Due to the page limit, we could not give all the diagrams and visualisation of the benchmark results in the article. They are available here: