Program of VERIFY

Tuesday, July 20th

Tuesday's program is also available with abstracts and side by side with other events.

08:50‑10:00 Welcome by the Chairs. Session 1
Location: IF 4.31+4.33
08:50 Invited Talk
09:00 Cliff Jones (Newcastle University, UK)
Abstractions Before Proofs
10:30‑12:30 Session 2: Verification in Various Domains
Location: IF 4.31+4.33
10:30 Angelo Brillout, Daniel Kroening, Philipp Ruemmer and Thomas Wahl
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
11:10 Shuling Wang and Xu Wang
Proving Four-Slot Algorithm Using Ownership Transfer
11:50 Michael von Tessin
Towards High-Assurance Multiprocessor Virtualisation
14:00‑15:00 Session 3: Invited Talk
Location: IF 4.31+4.33
14:00 Véronique Cortier (LORIA INRIA-Lorraine, France)
Verification of Security Protocols
15:30‑16:50 Session 4: Verification of IT-Security
Location: IF 4.31+4.33
15:30 Mark Bickford
Automated Proof of Authentication Protocols in a Logic of Events
16:10 Bernhard Beckert, Daniel Bruns and Sarah Grebing
Mind the Gap: Formal Verification and the Common Criteria
Wednesday, July 21st

Wednesday's program is also available with abstracts and side by side with other events.

09:00‑10:00 Session 5: Invited Talk
Location: IF 4.31+4.33
09:00 André Platzer (Carnegie Mellon University, USA)
Real Analysis for Complex Systems
10:30‑12:30 Session 6: Verification Techniques and Tools
Location: IF 4.31+4.33
10:30 Joe Hurd
Composable Packages for Higher Order Logic Theories
11:10 Andrei Lapets
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
11:50 Alessandro Carioni, Silvio Ghilardi and Silvio Ranise
MCMT in the Land of Parametrized Timed Automata
14:00‑15:00 Session 7: Software Security and Software Testing — ATTENTION: Session starts at 13:50!
Location: IF 4.31+4.33
14:00 13:50 Daniel Wasserrab and Denis Lohner
Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
14:30 Enrico Giunchiglia , Massimo Narizzano , Gabriele Palma and Alessandra Puddu
Automatic generation of high quality test sets via CBMC
15:30‑17:00 Session 8: Panel Discussion
Location: IF 4.31+4.33
15:30 Riccardo Focardi, Andrew Gordon, Reiner Hähnle, Cliff Jones, Mark Ryan, Johann Schumann
Panel Discussion: Formal Methods for/in/as Industry