Jul 04, 2017: Jaco van de Pol: Generation of Sequential and Parallel Model-Checking Benchmarks

July 04, 2017Generation of Sequential and Parallel Model-Checking Benchmarks
Room: Hal B 2BJaco van de Pol
12:30-13:30
Joint work with Marc Jasper, Jeroen Meijer, Jaco van de Pol, Bernhard Steffen,
Invited lecture at ACSD/Petri Nets 2017
Competitions and challenges can lead to scientific progress, since a whole
community wants to produce the best results and starts building upon
each other’s achievements.
The problem is how to generate benchmark problems that are really
hard to solve, but for which the solutions are still known. We show how to
solve this by synthesis and property-preserving transformations. In this
way, the RERS challenge generates sequential C-code and parallel
models, guaranteeing the validity of a number of predefined LTL or CTL
properties.
Among the advanced techniques used are: synthesis algorithms, model
checking, SAT solving, code motion, and refinement of modal transition 
systems.