VerifyThis Competition
About
VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015—2022. The challenge problems and solutions of previous competitions are available in the archive.
The competition will offer a number of challenges presented in natural language and pseudo code. 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 have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
Organizers
- external pageXavier Deniscall_made, Université Paris-Saclay
- external pageStephen Siegelcall_made, University of Delaware
More information
Steering Committee
- external pageMarieke Huismancall_made, University of Twente, the Netherlands
- external pageRosemary Monahancall_made, Maynooth University Maynooth, Ireland
- Peter Müller, ETH Zurich, Switzerland
- external pageMattias Ulbrichcall_made, Karlsruhe Institute of Technology, Germany
Contact
Email:
Web: http://verifythis.ethz.ch
Related Events and Activities
Related events are the Verified Software Competition (VSComp: external pagehttp://sites.google.com/a/vscomp.org/main/call_made, external pagehttps://sites.google.com/site/vstte2012/competcall_made, external pagehttp://www.vscomp.orgcall_made) held online and the external pageCompetition on Software Verificationcall_made focusing on evaluating systems in a way that does not require user interaction. SV-COMP is associated with TACAS.
VerifyThis is also a collection of verification problems (and solutions). Its counterpart is external pageVerifyThuscall_made—a distribution of deductive verification tools for Java-like languages, bundled and ready to run in a VM. Both were created with support from external pageCOST Action IC0701call_made.
A workshop on comparative empirical evaluation of reasoning systems external pageCOMPARE2012call_made was held on June 30th at IJCAR 2012 in Manchester. Competitions were one of the main topics of the workshop.