CPP

I will discuss the importance, uses, and future directions of formal verification from the point of view of a mathematical foundationalist. These include issues of certainty, proof structure, and (finitary) completeness and decidability.

Harvey Friedman

Ohio State University

In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higher-order representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.

Arthur Charguéraud

I am a full-time researcher at Inria. I am based in Saclay, in the Toccata team, also part of the VALS team. I am also involved in the DeepSea project at Inria Paris. My research interests span from programming languages to mechanized proofs.

We provide concrete evidence that floating-point computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floating-point arithmetic for the verification of properties of floating-point computations in C programs. To this end, we develop a framework to automatically compute real-number expressions of C floating-point computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energy-efficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floating-point rounding errors and energy-efficient approximations of square root and sine.

Tahina Ramananandro

Paul Mountcastle

Benoit Meister

Richard Lethin

In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used to verify real algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and code generator of Isabelle/HOL.

As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra’s algorithm.

Peter Lammich

Technische Universität München

I am a researcher (post-doc) at the chair for logic and verification of Prof. Tobias Nipkow. My main research interest is the production of verified software by a top-down refinement process. For this, I’m using the theorem prover Isabelle/HOL, for which I have developed the Isabelle Refinement Framework and the Isabelle Collection Framework. Other research interests include the automatic analysis of models for concurrent programs, and the mechanical verification of the analysis algorithms. To this end, I have explored dynamic pushdown networks, a model for concurrent programs with thread creation and locks as synchronization primitive. Moreover, we have developed the fully verified CAVA LTL model checker. Recently, I have also worked on modeling web-services in Isabelle/HOL, and formally verifying their information flow security properties. As a demonstrator, we have developed the conference management system CoCon, that has formally verified information flow properties

This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency.

Evgenii Kotelnikov

Chalmers University of Technology

Laura Kovacs

Chalmers University of Technology

Giles Reger

University of Manchester

Andrei Voronkov

University of Manchester

Hammers are tools for empolying external automatic theorem provers (ATPs) to improve automation in formal proof assistants. Strong automation can greatly ease the task of developing formal proofs. An essential component of any hammer is the translation of the logic of a proof assistant to the format of an ATP. Formalisms of state-of-the-art ATPs are usually first-order, so some method for eliminating lambda-abstractions is needed. We present an experimental comparison of several combinatory abstraction algorithms for HOL(y)Hammer – a hammer for HOL Light. The algorithms are compared on the HOL Light standard library extended with a library for multivariate analysis. We succeeded in developing algorithms which outperform both lambda-lifting and the simple Schonfinkel’s algorithm used in Sledgehammer for Isabelle/HOL. This visibly improves the ATPs’ success rate on translated problems, thus enhancing automation in proof assistants.

Lukasz Czajka

University of Innsbruck

The Isabelle/Isar language has been heavily inspired by the Mizar style, however already from the beginning it has been different in many ways and it has been evolving in different directions than the syntax the Mizar language. These differences were mostly motivated by the particular needs of integration with Isabelle at a particular time, in particular in order to make various proof tactics and other techniques associated with the LCF style available.

In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the meta-logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how meta-level types can be used to differenciate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the Tarski-Groethendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Pure definition syntax. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizar-style formalization, with cluster inferences and “by” steps performed manually.

Cezary Kaliszyk

University of Innsbruck

Karol Pąk

University of Bialystok, Institute of Computer Science

Josef Urban

This paper shows a construction of real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial at real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.

Wenda Li

University of Cambridge

China

Lawrence Paulson

Cambridge University

We describe the formalisation in Coq of a proof that the numbers e and pi are transcendental. This is the first formalized proof of transcendance for pi. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of pi relied extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials. In the paper, we describe the various original aspects of the work: orchestrating a development based on several libraries, designing a new library for multivariate polynomials, and specialized developments performed solely for this proof. Apart from achieving a landmark result, this work also teaches lessons about the evolution of modern formalized mathematics.

Sophie Bernard

INRIA

Yves Bertot

INRIA

France

Laurence Rideau

INRIA

Pierre-Yves Strub

IMDEA Software Institute

Spain

In automated complexity analysis of term rewriting, estimating the growth rate of the values in A n – for a fixed matrix A and increasing n – is of fundamental interest. This growth rate can be exactly characterized via A’s Jordan normal form (JNF). We formalized this result in our library IsaFoR and our certifier CeTA, and thereby improve the support for certifying polynomial bounds derived by (untrusted) complexity analysis tools. To this end, we develop a new library for matrices that admits to conveniently work with block matrices. Besides the mentioned complexity result, we formalize Gram-Schmidt’s orthogonalization algorithm and Schur decomposition in order to prove existence of JNFs. We also provide a uniqueness result for JNFs which allows us to compute Jordan blocks for individual eigenvalues. In order to determine eigenvalues automatically, we moreover formalize Yun’s square-free factorization algorithm.

René Thiemann

University of Innsbruck

Akihisa Yamada

We formalize an algorithm to change the representation of a polynomial to a Newton power series. This provides a way to compute efficiently polynomials which roots are the sums or products of roots of other polynomials, and hence provide a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of partial power series and develop an abstract theory of poles of fractions.

Cyril Cohen

Boris Djalal

INRIA

Dependent type theory is a powerful and expressive language for writing mathematical expressions and proofs, but careful design, engineering, and hard work are needed to put the theory into practice. In this talk, I will discuss some of the ideas and techniques that have been used in the design of the Lean theorem prover, a new proof system based on dependent type theory that aims to make the theorem proving process more natural, convenient, and efficient.

Leonardo De Moura

Microsoft Research, Redmond

Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of self-driving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundness-critical and extra logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live deterministic programs from liveness proofs for nondeterministic programs.

This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms – syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.

Nathan Fulton

Carnegie Mellon University

André Platzer

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all results in a new proof assistant, Lean.

Floris van Doorn

Carnegie Mellon University

I am currently a third year Ph.D. student in the Philosophy Department at Carnegie Mellon University. My advisor is Jeremy Avigad and I am also working together with Steve Awodey. I am enrolled in the Pure and Applied Logic program.

I previously studied at the Utrecht University in the Netherlands where I received a B.Sc. in Mathematics, a B.Sc. in Physics and a M.Sc. in Mathematics. My master thesis is Explicit convertibility proofs in Pure Type Systems supervised by Freek Wiedijk at the Radboud University Nijmegen. I was also trainer for the Dutch Mathematical Olympiad.

This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories a la Martin-Lof) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer’s Continuity Principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl’s meta-theory using our formalization of Nuprl in Coq and show how we can reflect these meta-theoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl’s key meta-theoretical properties, in particular consistency and the congruence of Howe’s computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer’s continuity theorem and bar induction on monotone bars.

Vincent Rahli

SnT

Mark Bickford

Cornell University

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine- checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework.

Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi- calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.

Johannes Å. Pohjola

Uppsala University

Joachim Parrow

Uppsala University

We present the first formal verification of the Raft consensus protocol, a critical component of many distributed systems. We proved that our implementation is a linearizable replicated state machine, which required iteratively discovering and proving nSysInv system invariants. Our verified implementation can be extracted and run on real networks.

The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariant strengthening patterns into custom induction principles, proves higher-order lemmas that show any property proved about a particular component imply analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.

Doug Woos

University of Washington

United States

James R. Wilcox

University of Washington

United States

Steve Anton

University of Washington

Zachary Tatlock

University of Washington, Seattle

United States

Michael D. Ernst

University of Washington

Thomas Anderson

University of Washington

We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.

Michel St-Martin

University of Ottawa

Amy Felty

University of Ottawa

Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the control-flow of a program.

In this paper, we formally verify in Coq an advanced code obfuscation called control-flow graph flattening, that is used in state-of-the-art program obfuscators. Our control-flow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.

Sandrine Blazy

IRISA / University of Rennes 1

Alix Trieu

ENS Rennes

Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic low-level language with linear sequential composition and lexically scoped gotos defined with a small-step semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.

Steven Schäfer

Sigurd Schneider

Saarland University

Gert Smolka

Saarland University

Food and drink accented by a brief presentation on the new initiative “The Science of Deep Specification,” sponsored by the U.S. National Science Foundation. Learn about this project that aims to catalyze more use of proof assistants for system verification at scale. Tickets included with CPP registration, with a limited number available for others on request.