| Tuesday, 24th September 2019 Verified Software Workshop Programme and Speaker list Photos of the two days | |
| 09:25-09:30 | Welcome by Philippa Gardner (Imperial College London, Director of VeTSS) and Christie Marr, (Deputy Director, Isaac Newton Institute for Mathematical Sciences) |
| 09:30-10:15 | Andreas Rossberg, Dfinity Foundation. “Language Formalisation Goes Mainstream” Slides |
| 10:15-11:00 | Ming Fu, Huawei. “Taking Formal Verification of Systems Software from Academia to Industry” |
| 11:00-11:30 | BREAK, Tea & Coffee |
| 11:30-12:15 | Peter Sewell, Cambridge University. “Fixing the Foundations with Semantics and Capabilites: ARM, RISC-V, and CHERI” Slides |
| 12:15-12:30 | Robert Watson, Cambridge University. “Technology Transition for CHERI – Opportunities for Research” Slides and recording of the talk. |
| 12:30-13:00 | Lightning Talks |
| 13:00-14:00 | LUNCH and Poster session |
| 14:00-14:45 | Jim Woodcock, University of York. “Verification Challenges” Slides and recording of the talk. |
| 14:45-15:30 | Future Challenges Discussion: Tony Hoare, John Goodacre and Philippa Gardner |
| 15:30-16:00 | BREAK, Tea & Coffee |
| 16:00-16:45 | Dan Zimmerman, Galois. “High Assurance Cryptography and Verifiable Elections” Slides |
| 16:45-17:30 | Peter O’Hearn, Facebook London and UCL. “Incorrectness Logic” |
| 17:30-18:30 | Lightning Talks |
| 19:30-22:00 | Workshop dinner at Westminster College. |
| Wednesday, 25th September 2019 | |
| 9:45-10:30 | Marta Kwiatkowska, Oxford University. “Safety verification for Deep Neural Networks with Provable Guarantees” Slides and recording of the talk. |
| 10:30-10:45 | Peter Davies, Thales. “What might I achieve with Verified Software in complex automotive systems?” Slides and recording of the talk. |
| 10:45-11:15 | BREAK, Tea & Coffee |
| 11:15-12:00 | Joost-Pieter Katoen, RWTH Aachen University. “Separation Logic Goes Random” Slides and recording of the talk. |
| 12:00-12:45 | Gustavo Petri, Arm Ltd. “Verification at Arm: a few case studies” Slides and recording of the talk. |
| 12:45-13:45 | LUNCH and Poster session |
| 13:45-14:30 | Sandrine Blazy, Inria Rennes. “Formal Verification of a Constant-Time Preserving C Compiler” Slides |
| 14:30-14:45 | Scott Owens, University of Kent (VeTSS). “Building Trustworthy Software with CakeML” |
| 14:45-15:00 | Conrad Watt, Cambridge University. “WebAssembly: Mechanisation, Security, and Concurrency” Slides and recording of the talk. |
| 15:00-15:15 | Brijesh Dongol, University of Surrey (VeTSS). “Mechanised Owicki-Gries Proofs for C11” Slides and recording of the talk. |
| 15:15-16:00 | Jeremy B, National Cyber Security Centre. “Verification for High Assurance Systems” |
| 16:00-16:30 | END OF WORKSHOP, Tea & Coffee |