LTSmin wins RERS challenge

Jaco van de Pol won the first prize in the RERS challenge at the ISOLA conference at Crete. The assignment was to check 100 properties on 15 C-programs with a PLC-like flat control structure including integer arithmetic. The programs were up to 6 MB large, with state spaces over 1 billion states.

The winning strategy was to transform the programs to Promela and check the properties with the multi-core LTL engine developed by Alfons Laarman, on a cluster of machines including a 48-core machine with 148 GB internal shared memory.

This was a free-style challenge. Our high-performance exhaustive analysis with LTSmin had to compete with approaches using BDDs, static analysis, constraints and symbolic execution.

October 18, 2012
Go to the news overview.