Wednesday, June 27
8:30 - 9:00
Registration
09:00 - 09:30
Introduction
Sound Static Analysis: 5-point seat belts for your code
by Paul E. Black, National Institute of Standards and Technology (NIST)
SESSION 1. ANALYSIS OF LEGACY CODE
09:30 - 10:30
Keynote
If it works, it’s legacy: analysis of legacy code
by David A. Wheeler, Institute for Defense Analyses
10:30 - 11:00
Coffee Break
11:00 - 11:30
Proving sequential properties of unmodified Linux kernel code
by Alexey Khoroshilov, Linux Verification Center of ISPRAS
11:30 - 12:00
Proving security properties in software of unknown provenance
by Ben Hocking, Dependable Computing
12:00 - 12:30
The Q-compiler for verifying high-consequence controls
by Jon Aytac, Sandia National Labs
12:30 - 13:00
Applying formal methods to existing software: what can you expect?
by Benjamin Monate, TrustInSoft
13:00 - 14:30
Lunch Break
Session 2. Use in new developments
14:30 - 15:30
Keynote
Trends in automated verification
by K. Rustan M. Leino, Amazon
15:30 - 16:00
Reimplement? Reuse? Both! — trustworthy systems with Genode and SPARK
by Alexander Senier, Componolit
16:00 - 16:30
Coffee Break
16:30 - 17:00
Mixing formal methods to increase robustness against cyber-attacks
by Laurent Voisin, Systerel
17:00 - 17:30
Enhance verification using ghost code
by Claire Dross, AdaCore
17:30 - 18:00
A formally verified floating-point implementation of the Compact Position Reporting algorithm
by Mariano M. Moscato, National Institute of Aerospace
18:00 - 20:00
Cocktail Reception at Holiday Inn




Thursday, June 28Session 3. Accountable software quality
09:00 - 10:00
Keynote
Lessons from verifying legacy Java code for C++ specification & verification
by David Cok, Visiting Research Engineer at CEA and Independent Consultant
10:00 - 10:30
Soundness, evidence and discipline in high-assurance software
by Roderick Chapman, Protean Code Limited
10:30 - 11:00
Coffee Break
11:00 - 11:30
Runtime verification of security properties with E-ACSL
by Julien Signoles, CEA LIST, Software Security and Reliability Lab
11:30 - 12:00
Industrial use of Formal Methods: a feedback from various experiments with Frama-C
by David Mentré, Mitsubishi Electric R&D Centre Europe (MERCE)
12:00 - 12:30
Practical application of SPARK: a business case and roadmap for new users
by Stuart Matthews, Altran
12:30 - 14:00
Lunch Break
14:00 - 14:30
Proving memory safety of C programs
by Henny Sipma, Kestrel Technology, LLC
14:30 - 15:00
Reflections on industrial use of Frama-C
by Joe Kiniry and Daniel Zimmerman, Galois
15:00 - 15:30
Coffee Break
SESSION 4. Tutorials
15:30 - 17:00
Frama-C & SPARK Tutorials and Exhibition