Updates

  • 22/10/16 Solutions uploaded
  • 20/08/16 Parallel problems replaced
  • 07/08/16 Parallel problems released
  • 20/06/16 workshop date annouced
  • 13/06/16 Parallel release announced
  • 01/05/16 Problems up

Important Dates:

  • 09/10/16
       RERS workshop at ISoLA
  • 31/05/16
       Release Ranking Details
  • 01/05/16 - 15/09/16
       Challenge Phase
  • 01/09/16 - 15/09/16
       Solution Submission
  • 07/08/16 - 15/09/16
       Release Parallel Problem

Download LTL Problems

Due to confusion about the semantic interpretation of the modulo operator and the integer range: the C code is to be interpretet as C99 and the inter range for all integers is asumed to be 32 bit.

It is planned to publish an STTT special section on RERS 2016. Winning and interesting approaches will be invited to publish a paper on their challenge approach and contribution. Each participant is invited to shortly present his or her approach on the challenge at the RERS meeting.

The bronze, silver and gold problems mark the level of difficulty. One Achievement is possible for each color, the most difficult level will be awarded. For further information please take a look at the rewards and achievements page.

For further information about the code layout please read the Java-code and C99-code description. Please take note of our behavioral semantics when analyzing the problems, a detailed description can be found on the problem description page. Please note that the syntax and semantic of the properties varies from the parallel problems.


The problems are provided as zip containing all LTL problems. Detailed solutions for the problems (with counterexamples) can be donwloaded as a zip file.


The table provides an overview of the dificulty of each problem.
size plain, simple arithmetic, medium data structures, hard
small Problem1 Problem2 Problem3
medium Problem4 Problem5 Problem6
large Problem7 Problem8 Problem9