VerifyThis 2016 - 5th Verification Competition

VerifyThis is a series of program verification competitions held earlier at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015. 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.
Organizers: Marieke Huisman, Vladimir Klebanov, Rosemary Monahan