http://lorentzcenter.nl/lc/web/2019/1115/info.php3?wsid=1115&venue=Snellius
During the workshop, to be able to offer a broad and diverse set of verification challenges, we are collecting submissions of ideas for verification challenges and problems related to pointer-manipulating software. We welcome both problems of academic interest as well as challenges based on themes that are relevant in industry. We encourage suggestions at any level of detail, including submissions without a fully worked out verification task.
- a problem is specified at least by an informal statement of the algorithm to be implemented (optionally with complete or partial pseudo or source code) and of the requirement(s) (optionally as a formal safety/functional correctness/... property) to be verified;
- a problem should be solvable, at least in part, within a 60-90 minute time slot by an experienced user. Alternatively, "hard" problems that one can think the whole week about are also of interest;
- submission of reference solutions is welcome but not mandatory;
- problems should preferably be language-independent. Those that are mainly suitable for specific languages or tools or that exhibit specific features such as concurrency or higher-order functions should be clearly identified as such;
- problems that contain several sub-problems or other means of difficulty scaling are especially welcome; and
- the organizers reserve the right (but no obligation) to discuss the problems in the meeting, either as submitted or with modifications.
Proposals can be submitted via Github. This is done as follows:
- Fork the repository
- Create a new directory called
challenge_name - Put a Markdown file called
README.mdin that directory that describes the challenge, together with any number of additional files. - Make a pull request.
The following competitions are targeted at related verification challenges, though not necessarily dealing only with pointer software:
- Separation Logic Competition (SL-COMP)
- Competition on Software Verification (SV-COMP) and its Collection of Verification Tasks
- VerifyThis
- Verified Software Competition
Another related activity is the Dagstuhl Seminar 14171 on "Evaluating Software Verification Systems: Benchmarks and Competitions".
- Lennart Beringer (Princeton University)
- Robbert Krebbers (TU Delft)
- Thomas Noll (RWTH Aachen University)
- Makoto Tatsuta (National Institute of Informatics)