Keynote Speakers
Nadia Polikarpova
University of California, San Diego
(joint with LICS)
Title: Synthesis of Safe Pointer-Manipulating Programs
Abstract:
Low-level pointer-manipulating code is ubiquitous in operating systems, networking stacks, and browsers, which form the backbone of our digital infrastructure.
Unfortunately, this code is susceptible to many kinds of bugs, which lead to crashes and security vulnerabilities. Read More
Andrei Popescu
University of Sheffield
Title: Bounded-Deducibility Security
Abstract:
Starting from 2013, together with colleagues I have developed a framework for the specification and verification of information-flow security. The framework is called Bounded-Deducibility (BD) Security because it generalises Sutherland’s notion of Nondeducibility: from entirely preventing to only bounding the allowed flows of information. It was born from the challenges of expressing fine-grained confidentiality policies, as required by many multi-user web-based systems.Read More
Magnus Myreen
Chalmers
Title: The CakeML Project’s Quest for Ever Stronger Correctness Theorems
Abstract:
The CakeML project has developed a proof-producing code generation
mechanism for HOL4, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them. Read More