The workshop will be in Maison de la Chimie, room 234 (2nd floor).



Session 1

Chair: Dirk Beyer
9:00–10:00 Invited talk by Matthias Heizmann and Andreas Podelski
Floyd-Hoare annotations in the Ultimate program analysis framework

We present how one can utilize Floyd-Hoare annotations to ensure the reliability of algorithmic verifica tion through the software verification tool chain Ultimate Automizer. Ultimate Automizer computes a pro of for a single sample trace of the program and then generalizes the proof to a proof for infinitely many traces. One can compute a Floyd-Hoare annotation for the full program from the proofs that result thi s way from a set of sample traces. Using the tool Ultimate Referee one can then check the validity of the Floyd-Hoare annotation for the full program. We also present the extension of the approach to inter procedural program analysis.

10:00–10:30 Jan Strejček
YAML-Based Format for Violation Witnesses
(joint work with P. Ayaziová, D. Beyer, M. Lingsch Rosenfeld, and M. Spiessl)


Coffee break


Session 2

Chair: Dirk Beyer
11:00–11:30 Nian-Ze Lee
Bridging Hardware and Software Verification Witnesses
(joint work with D. Beyer and P.-C. Chien)
11:30–12:00 Frank Schüssele
Concurrency Correctness Witnesses with Ghosts
(joint work with M. Bentele and D. Klumpp)




Session 3

Chair: Jan Strejček
14:00–15:00 Invited talk by Heike Wehrheim
Witnesses: From Proof Certificates to Cooperation Data

In software verification, witnesses are used to certify different sorts of data about programs, e.g. their correctness or incorrectness. Due to witnesses' diversity they can be employed for various purposes. The talk will reflect on the usage of witnesses as proof certificates in a proof-carrying code scheme and as artefacts in cooperative software verification.

15:00–15:30 Marian Lingsch Rosenfeld
YAML Witnesses in CPAchecker
(joint work with D. Beyer and M. Spiessl)


Coffee break


Session 4, Chair: Jan Strejček

Chair: Jan Strejček
16:00–16:30 Martin Spiessl
LIV: Invariant Validation Using Straight-Line Programs
(joint work with D. Beyer)
16:30–17:30 Discussion
(moderated by D. Beyer and J. Strejček)