VerifyThis 2019 : a program verification competition
- Dross, Claire AdaCore, Paris, France
- Furia, Carlo A Facoltà di scienze informatiche, Università della Svizzera italiana, Svizzera
- Huisman, Marieke University of Twente, Enschede, The Netherlands
- Monahan, Rosemary Maynooth University, Maynooth, Ireland
- Müller, Peter ETH Zurich, Zurich, Switzerland
-
19.05.2021
Published in:
- International Journal on Software Tools for Technology Transfer. - Springer. - 2021, vol. 23, p. 883–893
English
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 2 days ofwork. This report analyzes howthe 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.
- Language
-
- Italian
- Classification
- Computer science and technology
- License
- CC BY
- Open access status
- hybrid
- Identifiers
-
- RERO DOC 333682
- DOI 10.1007/s10009-021-00619-x
- ARK ark:/12658/srd1319373
- Persistent URL
- https://n2t.net/ark:/12658/srd1319373
Statistics
Document views: 90
File downloads:
- Furia_ijstftt_2021.pdf: 136