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.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