Royal Society Discussion and Scientific Meeting on Verified Trustworthy Software
Systems and the associated Specialist Meeting at Imperial College London.
The meeting, organised by Philippa Gardner with Mike Gordon FRS (Cambridge),
Greg Morrisett (Cornell), Peter O’Hearn (UCL, Facebook) and Fred Schneider (Cornell),
Specialist Meeting at Imperial College, Video recordings:
Peter Sewell, Computer Laboratory, University of Cambridge, UK
Warren Hunt, The University of Texas, USA
Anna Slobodova, Centaur Technology, Inc, USA
Andrei Sabelfeld, Chalmers University of Technology, Sweden
Lujo Bauer, Carnegie Mellon University, USA
Alexandra Silva, University College London, UK
Derek Dreyer, Max Planck Institute for Software Systems (MPI-SWS), Germany
Alastair Donaldson, Department of Computing, Imperial College London
Chris Hawblitzel, Microsoft Research, USA
Paul E. McKenney, IBM Linux Technology Center Hillsboro, Oregon
If your schedule allows for it, you can also watch the meeting sessions in one go:
Scientific Meeting, The Royal Society, recorded audio of the presentations:
Presentations (by order of appearance at the meetings)
- J Strother Moore, University of Texas at Austin, USA, Industrial hardware and software verification with ACL2. Slides
- Cédric Fournet, Microsoft Research, UK, miTLS: Verified Reference Implementations for TLS.
- Kathleen Fisher, Tufts University, USA, Using formal methods to eliminate exploitable bugs. Slides of the talk can be found here
- Neil White, Altran, UK, Formal verification: will the seeding ever flower? Slides
- Daniel Kroening, University of Oxford, UK, Program analysis using syntax-guided synthesis engines.
- Gerwin Klein, Data61 and UNSW Australia, Australia, Provably trustworthy systems. Slides
- Nickolai Zeldovich, MIT CSAIL, USA, Using Crash Hoare logic for certifying the FSCQ file system. Slides
- Mark Batty, University of Kent, UK, Industrial concurrency specification for C/C++ and Nvidia GPUs. Slides
- Peter O’Hearn, Facebook and University College London, UK, Moving fast with software verification.
- Fred B. Schneider, Cornell University, USA, Avoiding fatal flaws with formal methods.
- Alexey Gotsman, IMDEA Software Institute, Spain, A rigorous approach to consistency in cloud databases. Slides
- Michael Backes, Saarland University, Germany, imPACT: Privacy, Accountability, Compliance and Trust in tomorrow’s internet.
- Xavier Leroy, Inria Paris, France, Trust in programming tools: the formal verification of compilers and static analysers. Slides
- Marco Pistoia, IBM Thomas J. Watson Research Center, USA, Combining static analysis and machine learning for industrial-quality information-flow-security enforcement.
- Greg Morrisett, Cornell University, USA, Mind the gap: from crypto to code. Slides