Keynote Speakers

Nadia Polikarpova

University of California, San Diego

(joint with LICS)

Title: Synthesis of Safe Pointer-Manipulating Programs


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


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


Title: The CakeML Project’s Quest for Ever Stronger Correctness Theorems


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