VSL Publications

VerifyThis 2023: an International Program Verification Competition

Cite
Xavier Denis and Stephen F. Siegel. VerifyThis 2023: an International Program Verification Competition. In TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competition, Lecture Notes in Computer Science 14550, pp. 147-159. Springer, Cham, 2024.
Abstract
The 11th VerifyThis program verification competition took place on April 22, 2023, at ETAPS 2023 in Paris, France. Contestants were tasked with solving three verification challenges in real time, using any tools of their choice. The subjects of the challenges were (1) in-place reversal of a linked list, (2) ordered binary decision diagrams, and (3) a concurrent FIFO queue. Fifteen teams, each with 1 or 2 members, participated; all were required to be present on site. In this report, we summarize the three challenges and some of the notable solutions.
Downloads
  1. verifythis2023.pdf (preprint)
Related Links
  1. Published version (Springer web site)
  2. TOOLympics Challenge 2023 (Springer web site)
  3. VerifyThis 2023 Competition Archive
BibTeX 
@inproceedings{denis-siegel:2024:verifythis2023,
  author = {Xavier Denis and Stephen F.\ Siegel},
  title = {{V}erify{T}his 2023: an International Program
           Verification Competition},
  booktitle={TOOLympics Challenge 2023},
  volume = 14550,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  address = {Cham},
  editor = {Dirk Beyer and Arnd Hartmanns and Fabrice Kordon},
  year = {2024},
  pages = {147--159},
  doi = {10.1007/978-3-031-67695-6_5}
}
VSL | Publications