Benchmarks for the ProB (Dis)prover

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 here. A zip file containing all csv files is available 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

• Su and Abrial, Landing Gear Model 1, Provers alone
• Su and Abrial, Landing Gear Model 1, Tactics
• Su and Abrial, Landing Gear Model 2, Provers alone
• Su and Abrial, Landing Gear Model 2, Tactics
• Su and Abrial, Landing Gear Model 3, Provers alone
• Su and Abrial, Landing Gear Model 3, Tactics
• Hansen et. al., Provers alone
• Hansen et. al., Tactics
• Mammar and Laleau, Provers alone
• Mammar and Laleau, Tactics
• André, Attiogbé and Lanoix, Provers alone
• André, Attiogbé and Lanoix, Tactics

Further Models

• Colley, Canbus, Provers alone
• Colley, Canbus, Tactics
• Andriamiarina and Méry, Graphcoloring, Provers alone
• Andriamiarina and Méry, Graphcoloring, Tactics
• Wiegard, Stuttgart 21, Provers alone
• Wiegard, Stuttgart 21, Tactics

Summaries

• Tactics on Landing Gears
• Tactics on all Models
• Provers alone on Landing Gears
• Provers alone on all Models

Surplus of ProB

• Surplus of ProB (added last)
• Surplus of ProB (added first)