VerifyThis 2019: A Program Verification Competition (Extended Report)

TL;DR

How the participating teams fared on verification challenges was analyzed, what makes a verification challenge more or less suitable for the typical VerifyThis participants is reflected, and the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect are outlined.

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.

Figures (5)

• Figure 1: Algorithm to compute the maximal cutpoints of sequence .
• Figure 2: Algorithm to merge sorted sequences and into sorted sequence .
• Figure 3: Algorithm to compute the sequence of all left nearest smaller values of input sequence . The algorithm assumes that indexes start from $1$, and hence, it uses $0$ to denote that an index has no left neighbor.
• Figure 4: Cartesian tree of sequence $4\ 7\ 8\ 1\ 2\ 3\ 9\ 5\ 6$.
• Figure 5: Algorithm to multiply an input vector with a sparse matrix and store the result in the output vector . Input matrix is represented in the COO format as a list of triplets.