ITP on Monday, July 12th

09:00‑10:00 ITP Invited Talk
Chair: Sandip Ray
Location: AT LT5
09:00 Gerwin Klein (NICTA)
A Formally Verified OS Kernel. Now What?

Last year, the L4.verified project produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. In my presentation I will summarise the proof together with its main implications and assumptions, I will describe in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security, and I will explore further future research directions that open up with a formally verified OS kernel.

10:30‑12:30 Session 4
Chair: J Moore
Location: AT LT5
10:30 Joe Hendrix, Deepak Kapur and Jose Meseguer
Coverset Induction with Partiality and Subsorts: a Powerlist Case Study

Many inductive theorem proving tools generate induction schemes from the recursive calls appearing in recursively-defined functions defined in the specification. This strategy is called coverset induction in the context of algebraic specifications, and has proven quite useful in proving a wide variety of contexts. One challenge is that coverset induction typically requires the recursive function used to be a total function, while many operations are only meaningful on a subset of their inputs.

In this work, we present a generalized form of coverset induction that supports partial constructors and operations as specified in Maude using membership equational logic. We have implemented this in the Maude ITP, and used it to perform an extensive case study involving Powerlists -- a data structure introduced by Misra to elegantly formalize parallel algorithms. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about Powerlists can be naturally proven using coverset induction in the Maude ITP.

11:00 Michaël Armand, Benjamin Grégoire, Arnaud Spiwack and Laurent Théry
Extending Coq with Imperative Features and its Application to SAT Verification

Coq has within its logic a programming language that can be used to replace many deduction steps into a single computation, this is the so-called reflection. In this paper, we present two extensions of the evaluation mechanism that preserve its correctness and make it possible to deal with cpu-intensive tasks such as proof checking of SAT traces.

11:30 Moa Johansson, Lucas Dixon and Alan Bundy
Case-Analysis for Rippling and Inductive Proof

Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements to be proved automatically. The new contribution is that our method also supports case-analysis on datatypes. By locating the case-analysis as a step within rippling we also maintain the termination of rippling. The work has been implemented in IsaPlanner and used to extend the existing inductive proof method. We evaluate this extended prover on a large set of examples from Isabelle's theory library as well as problems from the inductive theorem proving literature. We find that this leads to a significant improvement in the coverage of inductive theorem proving. The main limitations of the extended prover are also identified. These highlight the need for advances in the treatment of assumptions during rippling and when conjecturing lemmas.

12:00 Panagiotis Manolios and Daron Vroon
Interactive Termination Proofs using Termination Cores

Recent advances in termination analysis have yielded new methods and tools that are highly automatic. However, when they fail, even experts have difficulty understanding why and determining how to proceed. In this paper, we address the issue of building termination analysis engines that are both highly automatic and easy to use in an interactive setting. We consider the problem in the context of ACL2, which has a first-order, functional programming language. We introduce the notion of a termination core, a simplification of the program under consideration which consists of a single loop that the termination engine cannot handle. We show how to extend the Size Change (SC) algorithm so that it generates termination cores when it fails to prove termination, with no increase to its complexity. We show how to integrate this into the Calling Context Graph (CCG) termination analysis, a powerful SCT-based automatic termination analysis that is part of the ACL2 Sedan. We also present several new, convenient ways of allowing users to interface with the CCG analysis, in order to guide it to a termination proof.

14:00‑15:00 Session 5
Chair: Gerwin Klein
Location: AT LT5
14:00 Gilles Barthe, Benjamin Grégoire and Santiago Zanella Béguelin
Programming language techniques for cryptographic proofs

CertiCrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. CcertiCrypt adopts the code-based paradigm, in which the statement of security, and the hypotheses under which it is proved, are expressed using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare logic, semantics-preserving program transformations) to assist in constructing proofs. Earlier publications of CertiCrypt provide an overview of its architecture and its main components, and describe its applications to signature and encryption schemes. This paper describes programming language techniques that arise specifically in cryptographic proofs. The techniques have been developed to complete a formal proof of the IND-CCA security of the OAEP padding scheme. In this paper, we illustrate their usefulness for showing the PRP/PRF Switching Lemma, a fundamental cryptographic result that bounds the probability of an adversary to distinguish a family of pseudorandom functions from a family of pseudorandom permutations.

14:30 David Cachera and David Pichardie
Proof Pearl: A Certified Denotational Abstract Interpreter

Abstract Interpretation proposes advanced techniques for static analysis of programs that raise specific challenges for machine-checked soundness proofs. Most classical dataflow analysis techniques iterate operators on lattices without infinite ascending chains. In contrast, abstract intepreters are looking for fixpoints in infinite lattices where widening and narrowing are used for accelerating the convergence. Smart iteration strategies are crucial when using such accelerating operators because they directly impact the precision of the analysis diagnostic. In this paper, we show how we manage to program and prove correct in Coq an abstract interpreter that uses iteration strategies based on program syntax. A key component of the formalisation is the introduction of an intermediate semantics based on a generic least-fixpoint operator on complete lattices and allows us to decompose the soundness proof in an elegant manner.

15:30‑17:00 Session 6
Chair: Pete Manolios
Location: AT LT5
15:30 Sol Swords and Warren Hunt
A Mechanically Verified AIG-to-BDD Conversion Algorithm

We present the mechanical verification of an algorithm for building a BDD from an AND/INVERTER graph (AIG). The algorithm uses two methods to simplify an input AIG using BDDs of limited size; it repeatedly applies these methods while varying the BDD size limit. One method is similar to dynamic weakening in that it replaces oversized BDDs by a conservative approximation; the other method introduces fresh variables to represent oversized BDDs. This algorithm is written in the executable logic of the ACL2 theorem prover. The primary contribution is the verification of our conversion algorithm. We state its correctness theorem and outline the major steps needed to prove it.

16:00 William Mansky and Elsa Gunter
A Framework for Formal Verification of Compiler Optimizations

In this article, we describe a framework for formally verifying the correctness of compiler optimizations. We begin by giving formal semantics to a variation of the TRANS language, which is designed to express optimizations as transformations on control-flow graphs using temporal logic side conditions. We then formalize the idea of correctness of a TRANS optimization, and prove general lemmas about correctness that can form the basis of a proof of correctness for a particular optimization. As a proof of concept, we present an implementation of the framework in Isabelle, along with a proof of correctness of an algorithm for converting programs into Static Single Assignment form.

16:30 Herman Geuvers, Adam Koprowski, Dan Synek and Eelis van der Weegen
Automated Machine-Checked Hybrid System Safety Proofs

We have developed a hybrid system safety prover, implemented in Coq using the abstraction method introduced by Alur, Dang and Ivančić (2006). The development includes: a formalization of the structure of hybrid systems; a set of utilities for the construction of an abstract system (consisting of decidable ``overestimators'' of abstract transitions and initiality) faithfully representing a (concrete) hybrid system; a translation of abstract systems to graphs enabling the decision of abstract state reachability using a certified graph reachability algorithm; a proof of an example hybrid system generated using this tool stack. The development critically relies on the computable real number implementation part of the CoRN library of formalized constructive mathematics in Coq. The obtained safety proofs are fully certified and don't use floating point real numbers, but arbitrary precise approximations of computable real numbers. It also uses a nice interplay between constructive and classical logic via the double negation monad.

17:00‑18:00 Business Meeting
Chair: Matt Kaufmann and Michael Norrish
Location: AT LT5