VerifyThis 2015 - 4th VerifyThis

VerifyThis is the successor of the program verification competitions held at FoVeOOS2011, FM2012 and the Dagstuhl seminar on Evaluating Software Verification Systems: Benchmarks and Competitions.
Its aims are:
to bring together those interested in formal verification,
to provide an engaging, hands-on, and fun opportunity for discussion,
to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated.
The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will focus on the input-output behavior of programs, yet it is at the discretion of participants to treat only aspects of requirements. Solutions will be judged for correctness, completeness, degree of automation, and elegance.
Organisers:
Marieke Huisman (M.Huisman-AT-utwente.nl)
Vladimir Klebanov (klebanov-AT-kit.edu)
Rosemary Monahan (Rosemary.Monahan-AT-nuim.ie).