Verified Software Workshop, INI, 2019

The Verified Software Workshop was held on Tuesday 24th September 2019 and Wednesday 25th September 2019 at the Isaac Newton Institute, Cambridge. The two day workshop on verified software, with talks by world-leading experts from academia, industry and government was hosted by the Newton Gateway to Mathematics in partnership with VeTSS.

Aims and Objectives

The workshop was a forerunner to the INI’s six-week summer programme on ‘Verified Software’ and aimed at bringing together verification, systems and security experts interested in formal analysis, industrialists interested in software validation, and government scientists interested in reliable software systems, and introduced them to the current generation of UK PhD students and postdocs. The challenge was to answer questions such as:

  • How do we construct software stacks with accurate mathematical models and provably predictable behaviour relative to these models?
  • Can we build mathematical models and proofs for verifying safety and security properties of complex software systems that operate cars and planes and manage financial transactions?
  • What theoretical advances are needed for modelling and analysing large software systems?
  • What language and semantic analysis tools can assist in the large-scale construction of verified software?
  • Can we create an ecosystem of high-quality verified software with well-defined interfaces and composition mechanisms?

Programme and Slides

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