Andreas Abel (Chalmers University), Coinduction in Agda using Copatterns and Sized Types
Agda, the dependently-typed programming and proof language based on Martin-Löf's Type Theory, now has a type-based productivity check for corecursively defined objects and functions. In this talk, the theoretical basis is explained and it practicality is explored via some case studies.
Amal Ahmed (Northeastern University), Compositional Compiler Verification for a Multi-language World
Nick Benton & Andrew Kennedy (MSR Cambridge), Generating Certified x86 Code in a Proof Assistant
Lars Birkedal (Aarhus University), Impredicative Concurent Abstract Predicates. Joint work with Kasper Svendsen. Based on paper published at ESOP 2014.
In this talk I present impredicative Concurrent Abstract Predicates – iCAP – a program logic for modular reasoning about concurrent, higher-order, reentrant, imperative code. Building on earlier work, iCAP uses protocols to reason about shared mutable state. A key novel feature of iCAP is the ability to define impredicative protocols; protocols that are parameterized on arbitrary predicates, including predicates that themselves refer to protocols. We demonstrate the utility of impredicative protocols through a series of examples, including the specification and verification, in the logic, of a spin-lock, a reentrant event loop, and a concurrent bag implemented using cooperation, against modular specifications.
Arthur Charguéraud (INRIA Saclay - Île-de-France), Interactive verification of stateful higher-order programs using characteristic formulae
Given the source code of a program, we automatically compute its characteristic formula, which is a logical formula that describes the semantics of the code without referring to its syntax. This formula can be exploited in a higher-order logic based proof assistant (e.g., Coq) to conduct interactive verification of arbitrarily-complex programs, in particular programs involving first-class functions and nontrivial use of effects. Characteristic formulae are based on Separation Logic specifications, thereby allowing for modular proofs.
Adam Chlipala (MIT), Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs
The foundational proof-carrying code (FPCC) paradigm involves distributing software modules with proofs that they adhere to specifications of interest to end users. When those specifications are detailed enough to fall under the umbrella of functional correctness, constructing the proofs presents a serious engineering challenge. As with software engineering, it becomes important to find abstraction and modularity techniques that facilitate reuse of work across many code + proof packages. In my talk, I will give an overview of Bedrock, a project to design and implement a practical trusted core of a FPCC platform, plus an ecosystem of example tools targeting it. Bedrock supports modular verification of assembly code via a notion of code + proof package inspired by the XCAP program logic. We have built higher-level language implementations (for an extensible C-like language, a language with an integrated notion of mutable abstract data types, and a DSL for database-backed XML web services) and associated reasoning tools (automation for higher-order separation logic and for reasoning about abstract data types at a higher level). The infrastructure has been used to do a complete modular verification of isolation properties for a software stack starting from simple nonblocking network operations and culminating in a multi-threaded, database-backed web service that has been deployed on mobile robots, and our ongoing work focuses on increasing the strength of such theorems while experimenting with higher-level programming notations, including general mathematical specifications via program synthesis.
Derek Dreyer (Max-Planck Institute for Software Systems), GPS: Navigating weak memory with ghosts, protocols, and separation
Compilers and CPUs routinely transform code in ways that are invisible to sequential code, but observable concurrently. These transformations weaken the abstraction of shared memory, for example allowing different threads to observe writes in different orders, which complicates the already-difficult task of reasoning about concurrency. Worse still, they render impotent our most effective weaponry: the sophisticated formal methods that have been developed to tame concurrency almost universally assume a strong (sequentially consistent) memory model. This talk will present GPS, a new program logic that provides a full-fledged suite of modern verification techniques for reasoning under a weak memory model. GPS includes a form of ghost state, rely-guarantee “protocols”, and separation logic –a combination that has been very fruitful for reasoning under strong memory. The logic is specifically geared for reasoning about the recent C/C++11 memory model. We demonstrate its effectiveness by applying it to challenging examples drawn from the Linux kernel, as well as lock-free data structures. We will also briefly discuss the proof of soundness for GPS, which has been formalized in the Coq proof assistant.
Philippa Gardner (Imperial College, London), Abstract Disjointness, Abstract Atomicity and Abstract Connectivity
Dan Ghica (University of Birmingham), Compiling functional programs to distributed architectures using abstract machine nets
We present new abstract machines for the execution of higher-order programs running in distributed architectures. They implement a generalised form of Remote Procedure Call that supports calling higher-order functions across node boundaries, without sending actual code. Our starting point are conventional abstract machines, such as SECD or Krivine, which implement reduction strategies for untyped applied lambda calculi. We successively add the features that we need for distributed execution and show the correctness of each addition. We construct two-level operational semantics, where the high level is a network of communicating machines, and the low level is given by local machine transitions. Using these networks, we arrive at our final system, networks of abstract machines.All the technical results have been formalised and proved correct in Agda and have been implemented in proof-of-concept compilers.
Martin Hofmann (Ludwig-Maximilians-Universität München), Abstract effects and proof-relevant logical relations. Joint work with Nick Benton, Microsoft Research Cambridge and Vivek Nigam, Uni Joao Pessoa
We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module to validate soundly more effect-based program equivalences than would be possible with previous semantics. Our semantics uses a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves two awkward problems caused by naive use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.
Xavier Leroy (INRIA Paris-Rocquencourt), Verified static analyses
Static analysis – the automatic determination of simple properties of a program – is the basis both for optimizing compilation and for verification of safety properties such as absence of run-time errors. To support the use of static analyses in verified compilers and in high-confidence verification environments, the analyses must be proved to be sound. In this talk, I will review some ongoing work in this direction in the CompCert and Verasco projects, in particular the construction and formal verification of a modular static analyzer based on abstract interpretation.
Greg Morrisett (Harvard University), Engineering Challenges for Modeling Languages
Magnus Myreen (University of Cambridge), CakeML: a verified implementation of ML
I will present the CakeML project. This project centres around a subset of ML that is carefully chosen to be easy to write programs in and convenient to reason about formally. I will talk about results so far, in particular, our a formally verified implementation of CakeML (a compiler and a read-eval-print loop) in 64-bit x86 machine code. The construction and verification of this implementation required both proofs of high-level programs (the parser, type inferencer and compiler) and low-level programs (the runtime in x86 machine code, its bignum library and garbage collector). We used a novel technique to produce much of the verified low-level code: we bootstrapped the verified compiler algorithm, within the logic, to produce the verified low-level implementation. At the workshop, I would also like to discuss the place of ML in high assurance software and also establish new collaborations. At the time of writing, this project is an active collaboration between Ramana Kumar at Cambridge (UK), Scott Owens at Kent (UK), Michael Norrish at NICTA (Australia), and myself, with a few others possibly joining soon.
David Pichardie (ENS Rennes), Atomicity Refinement for Verified Compilation
We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on out-of-order reorderings performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings, an impractical and non-scalable exercise. In this work we address this challenge with a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We validate the effectiveness of our approach by demonstrating the verified compilation of some non-trivial components of a realistic concurrent garbage collector.
Brigitte Pientka (Mc Gill), Programming logical relations proofs
We will survey Beluga, a dependently typed programming and proof environment. It supports specifying formal systems in the logical framework LF and directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding LF objects together with their surrounding context in programs and supports recursive types to state properties about LF objects and their contexts. Concentrating on a weak normalization proof, I will highlight several key aspects of Beluga and its design, in particular the power to support first-class substitutions and logical relations proofs. Taken together these examples demonstrate the elegance and conciseness of Beluga for specifying, verifying and validating proofs.
Peter Sewell (University of Cambridge), Before Certification: Engineering Validatable Models
Tarmo Uustalu (Tallin University of Technology), Precise qualification of effects with dependently typed monads
Viktor Vafeiadis (Max-Planck Institute for Software Systems), An Argument for Relaxed Program Logic
Program logic is not only useful for reasoning about programs, but also for understanding programming languages. In this talk, I will explain the C/C++ weak memory model through a sequence of concepts from program logic: ownership transfer, rely-guarantee, auxiliary variables, and modal operators.
Stephanie Weirich (University of Pennsylvania), Combining Proofs and Programs in a Dependently Typed Language
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Omega). Here, we combine these two approaches into a single dependently-typed language, called Zombie. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and certain program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.
Hongseok Yang (University of Oxford), Replicated Data Types: Specification, Verification, Optimality. Joint work with Sebastian Burckhardt at Microsoft Research Redmond, Alexey Gotsman at IMDEA Software Institute and Marek Zawirski at INRIA & UPMC-LIP6.
Geographically distributed systems often rely on replicated eventually consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as registers, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications, correctness proofs, and optimality results. In this talk, I will explain our framework for specifying replicated data types using relations over events and verifying their implementations using replication-aware simulations. The framework has been applied to existing implementations of data types with nontrivial conflict-resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). If time permits, I will also explain a novel technique for obtaining lower bounds on the worst-case space overhead of data type implementations and show how it can be used to prove optimality of the implementations of well-known data types.
Nobuko Yoshida (Imperial College, London), Idioms for Interaction and their applications in large distributed systems
We shall first talk how Kohei Honda invented the idea of session types. We shall then talk how Robin Milner, Honda and Yoshida started collaborations with industry to develop a web service protocol description language called Scribble and discovered the theory of multiparty session types through the collaborations. We then give a summary of our recent research developments on multiparty session types for verifying distributed and concurrent programs, and our collaborations with industry partners and a major, long-term, NSF-funded project (Ocean Observatories Initiatives) to provide an ultra large-scale cyberinfrustracture (OOI CI) for 25-30 years of sustained ocean measurements to study climate variability, ocean circulation and ecosystem dynamics. We talk about the recent developments in Scribble and the runtime session monitoring framework currently used in the OOI CI.
Francesco Zappa-Nardelli (INRIA Paris-Rocquencourt), Concurrency and compiler correctness
Steve Zdancewic (University of Pennsylvania), Vellvm: Verifying Transformations of the LLVM IR
The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses. In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics, including nondeterminism and its use of SSA representation. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and give two example applications: (1) formal verification of the SoftBound pass, which hardens C programs against memory safety errors, and (2) the mem2reg transformation, which promotes stack-allocated temporaries to registers and converts “trivial” SSA programs to “minimal, pruned” SSA programs. Vellvm, which is implemented in the Coq theorem prover, provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts. Our experimental results show that fully verified and automatically extracted implementations can yield competitive performance. This is joint work with Jianzhou Zhao and Milo Martin (both at Penn) and Santosh Nagarakatte (at Rutgers University).
