Verified Software Workshop Programme

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