  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.
