Program
9:00–10:30 | 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) |
10:30–11:00 | Coffee break |
11:00–12:00 | 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) |
12:00–14:00 | Lunch |
14:00–15:30 | 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) |
15:30–16:00 | Coffee break |
16:00–17:30 | Session 4, |
| 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) |