We have setup the challenge problems for Java and C almost identically. The main difference is that input and output symbols are given as strings in the Java setting and as plain numbers in the C setting (an explicit request from that community). Despite this difference, one can proceed exactly in the same fashion, e.g.:

• For solving the implicit problems, you might analyse the code for errors/exceptions/assertions labels. Each such label occuring in the code defines a reachability problem, which you can solve with the method of your choice. There are no limitations.
• The explicit problems, even if reminding of typical model checking problems, may also be dealt with in any fashion you like, e.g. dataflow analysis, symbolic execution, testing, learning, (statistical) model checking, run-time methods,....
• The challenge is free-style. You are allowed to patch the code in any way you like, but the validity has, of course, to be stated according to the original problems.
• You should first concentrate on the problems and properties you can master well. You do not have to give an anser to all problems. Of course, the more problems you can tackle, to more points you may be able to win, but please be aware, wrong answers have a big penalty!
• The weighting scheme gives you a way to express your personal confidence in your results. e.g. if you have found a feasable path to some error, this is safe, and you should weight it 9. Liveness properties or stating that certain errors are non-feasible is of course more risky.

Concerning the second form of ranking, please write a short summary of your approach, the encountered hurdles, your solutions, and your results. In these summaries, honesty, e.g. also concerning weaknesses of the employed methods, is important. Our challenge aims at profiling the various approaches and methods, which in particular means that weaknesses need to be identified. Of course, we are also very interested in new ideas and solutions that were motivated by the challenge.

If you have completed all (or some) tasks, we kindly request you to submit your solution in a CSV-style format. Solutions for each of the problems should be specified in the following way:

<spec1>,<answer1>,<confidence1>
<spec2>,<answer2>,<confidence2>
...

where

• spec is the problem specification identifier. This can either be a number ranging from 1 to 160, where numbers 1 through 59 correspond to the error labels, number 60 to the global error, and numbers 61 through 160 to the 100 LTL formulae. Or you can specify directly the LTL expression, or the name of the error label respectively.
• answer expresses whether or not you believe this error label to be reachable, or the respective LTL property to be satisfied. This may be expressed as true/false, yes/no or 1/0.
• confidence is the confidence with which you want to weight your solution, i.e., a number ranging from 0 to 9.

Please choose for each of the CSV-files a name which clearly identifies the respective problem. Alternatively, you may combine your results into a global CSV with 4 columns per row; the first one designating the number of the problem. Hence, a line in this file for a hypothetical problem 0 might look like this:

0, error_37, true, 7

You can submit your solutions by sending them to via mail.