Verified Software Workshop Programme

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