VerifyThis 2019: A Program Verification Competition (Extended Report)
Claire Dross, Carlo A. Furia, Marieke Huisman, Rosemary Monahan, Peter, M\"uller

TL;DR
VerifyThis 2019 was a competition emphasizing human expertise in program verification, involving diverse teams solving complex behavioral property challenges over two days, highlighting the difficulties in comparing varied approaches.
Contribution
This report documents the 8th VerifyThis competition, analyzing team performances, challenge suitability, and the challenges in comparing diverse verification methods.
Findings
Teams used different verification approaches.
Challenges varied in difficulty and suitability.
Comparison of approaches remains complex.
Abstract
VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something that lies beyond the capabilities of fully automatic verification, and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned two days of work. The report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Advanced Malware Detection Techniques · Software Reliability and Analysis Research
