Interactive Theorem Proving

We formalise a statement of Green’s theorem in Isabelle/HOL, which is its first formalisation to our knowledge. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. An interesting aspect of our formalisation is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to equivalences between paths.

HOL Zero is a basic theorem prover that aims to achieve the highest levels of reliability and trustworthiness through careful design and implementation of its core components. In this paper, we concentrate on its treatment of concrete syntax, explaining how it manages to avoid problems suffered in other HOL systems related to the parsing and pretty printing of HOL types, terms and theorems, with the goal of achieving well-behaved parsing/printing and Pollack-consistency. Included are an explanation of how Hindley-Milner type inference is adapted to cater for variable-variable overloading, and how terms are minimally annotated with types for unambiguous printing.

TRACER [8] is a tool for verifying safety properties of sequential C programs. TRACER attempts at building a finite symbolic execution graph which over-approximates the set of all concrete reachable states and the set of feasible paths.We present an abstract framework for TRACER and similar CEGAR-like systems [2, 3, 5, 6, 9]. The framework provides (1) a graph-transformation based method for reducing the feasible paths in control-flow graphs, (2) a model for symbolic execution, subsumption, predicate abstraction and invariant generation. In this framework we formally prove two key properties: correct construction of the symbolic states and preservation of feasible paths. The framework focuses on core operations, leaving to concrete prototypes to “fit in” heuristics for combining them.

We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronosOS: that the running task is always the highest-priority runnable task. The key differentiator of this verification is that the OS code itself runs with interrupts on, even within the scheduler, to minimise latency. Our reasoning includes context switching, interleaving with interrupt handlers and nested interrupts; and it is formalised in Isabelle/HOL, building on the Owicki-Gries method for fine-grained concurrency. We add support for explicit concurrency control and the composition of multiple independently-proven invariants. Finally, we discuss how scalability issues are addressed with proof engineering techniques, in order to handle thousands of proof obligations.

Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. Sulzmann and Lu have made available on-line what they call a “rigorous proof” of the correctness of their algorithm w.r.t. their specification; regrettably, it appears to us to have unfillable gaps. In the first part of this paper we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu’s algorithm always generates such a value (provided that the regular expression matches the string). We also prove the correctness of an optimised version of the POSIX matching algorithm. Our definitions and proof are much simpler than those by Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the second part we analyse the correctness argument by Sulzmann and Lu and explain why the gaps in this argument cannot be filled easily.

This paper describes progress with our agenda of formal verification of information-flow security for realistic systems. We present CoSMed, a social media platform with verified document confidentiality. The system’s kernel is implemented and verified in the proof assistant Isabelle/HOL. For verification, we employ the framework of Bounded-Deducibility (BD) Security, previously introduced for the conference system CoCon. CoSMed is a second major case study in this framework. For CoSMed, the static topology of declassification bounds and triggers that characterized previous instances of BD security has to give way to a dynamic integration of the triggers as part of the bounds.

The impossibility of distributed consensus with one faulty process is a result with important consequences for real world distributed systems e.g., commits in replicated databases. Since proofs are not immune to faults and even plausible proofs with a profound formalism can conclude wrong results, we validate the fundamental result named FLP after Fischer, Lynch and Paterson by using the interactive theorem prover Isabelle/HOL. We present a formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen Völzer’s paper A constructive proof for FLP. In addition to the enhanced confidence in the validity of Völzer’s proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization may serve as a starting point for similar proofs of properties of distributed systems.

The Incredible Proof Machine is an easy and fun to use program to conduct formal proofs. It employs a novel, intuitive proof representation based on port graphs, which is akin to, but even more natural than, natural deduction. In particular, we describe a way to determine the scope of local assumptions and variables implicitly. Our practical classroom experience backs these claims.

We present a proof of the fact that $$2^{n} \le {{\mathrm{lcm}}}\{1, 2, 3, \dots , (n+1)\}$$. This result has a standard proof via an integral, but our proof is purely number theoretic, requiring little more than list inductions. The proof is based on manipulations of a variant of Leibniz’s Harmonic Triangle, itself a relative of Pascal’s better-known Triangle.

We formally verify translations from two-way automata to one-way automata based on results from the literature. Following Vardi, we obtain a simple reduction from nondeterministic two-way automata to one-way automata that leads to a doubly-exponential increase in the number of states. By adapting the work of Shepherdson and Vardi, we obtain a singly-exponential translation from nondeterministic two-way automata to DFAs. The translation employs a constructive variant of the Myhill-Nerode theorem. Shepherdson’s original bound for the translation from deterministic two-way automata to DFAs is obtained as a corollary. The development is formalized in Coq/Ssreflect without axioms and makes extensive use of countable and finite types.

The class of stencil programs involves repeatedly updating elements of arrays according to fixed patterns, referred to as stencils. Stencil problems are ubiquitous in scientific computing and are used as an ingredient to solve more involved problems. Their high regularity allows massive parallelization. Two important challenges in designing such algorithms are cache efficiency and minimizing the number of communication steps between nodes. In this paper, we introduce a mathematical framework for a crucial aspect of formal verification of both sequential and distributed stencil algorithms, and we describe its Coq implementation. We present a domain-specific embedded programming language with support for automating the most tedious steps of proofs that nested loops respect dependencies, applicable to sequential and distributed examples. Finally, we evaluate the robustness of our library by proving the dependency-correctness of some real-world stencil algorithms, including a state-of-the-art cache-oblivious sequential algorithm, as well as two optimized distributed kernels.

Formal analysis of ordinary differential equations (ODEs) and dynamical systems requires a solid formalization of the underlying theory. The formalization needs to be at the correct level of abstraction, in order to avoid drowning in tedious reasoning about technical details. The flow of an ODE, i.e., the solution depending on initial conditions, and a dedicated type of bounded linear functions yield suitable abstractions. The dedicated type integrates well with the type-class based analysis in Isabelle and we prove advanced properties of the flow, most notably, differentiable dependence on initial conditions via the variational equation and a rigorous numerical algorithm to solve it.

Types in Higher-Order Logic (HOL) are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its soundness. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.

We present a formalization of the Ford-Fulkerson method for computing the maximum flow in a network. Our formal proof closely follows a standard textbook proof, and is accessible even without being an expert in Isabelle/HOL — the interactive theorem prover used for the formalization. We then use stepwise refinement to obtain the Edmonds-Karp algorithm, and formally prove a bound on its complexity. Further refinement yields a verified implementation, whose execution time compares well to an unverified reference implementation in Java.

We present a formalization of Cauchy’s residue theorem and two of its corollaries: the argument principle and Rouché’s theorem. These results have applications to verify algorithms in computer algebra and demonstrate Isabelle/HOL’s complex analysis library.

In reasoning about effectful computations, it often suffices to focus on the effect-free parts. We present a package for automatically lifting equations to effects modelled by applicative functors. It exploits properties of the concrete functor thanks to a modular classification based on combinators. We formalise the meta theory and demonstrate the usability of our Isabelle/HOL package with two case studies. This is a first step towards practical reasoning with effectful computations.

Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis.This paper presents an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq formal system. Our approach is not based on traditional quadrature methods such as Newton-Cotes formulas. Instead, it relies on computing and evaluating antiderivatives of rigorous polynomial approximations, combined with an adaptive domain splitting. This work has been integrated to the CoqInterval library.

This paper presents the first formalization of three classic confluence criteria for first-order term rewrite systems by Huet and Toyama. We have formalized proofs, showing that (1) linear strongly closed systems, (2) left-linear parallel closed systems, and (3) left-linear almost parallel closed systems are confluent. The third result is extended to commutation. The proofs were carried out in the proof assistant Isabelle/HOL as part of the library IsaFoR and integrated into the certifier CeTA, significantly increasing the number of certifiable proofs produced by automatic confluence tools.

In a new approach, functional correctness specifications of insert/update and delete operations on search trees are expressed on the level of lists by means of an inorder traversal function that projects trees to lists. With the help of a small lemma library, functional correctness and preservation of the search tree property are proved automatically (in Isabelle/HOL) for a range of data structures: unbalanced binary trees, AVL trees, red-black trees, 2-3 and 2-3-4 trees, 1-2 brother trees, AA trees and splay trees.

Our language Cogent simplifies verification of systems software using a certifying compiler, which produces a proof that the generated C code is a refinement of the original Cogent program. Despite the fact that Cogent itself contains a number of refinement layers, the semantic gap between even the lowest level of Cogent semantics and the generated C code remains large.In this paper we close this gap with an automated refinement framework which validates the compiler’s code generation phase. This framework makes use of existing C verification tools and introduces a new technique to relate the type systems of Cogent and C.

A formalization in Isabelle/HOL of the resolution calculus for first-order logic is presented. Its soundness and completeness are formally proven using the substitution lemma, semantic trees, Herbrand’s theorem, and the lifting lemma. In contrast to previous formalizations of resolution, it considers first-order logic with full first-order terms, instead of the propositional case.

Operational transformation (OT) is an approach to concurrency control in groupware editors first proposed by C. Ellis and S. Gibbs in 1989. Google Wave and Google Docs are examples of better known OT-based systems and there are many other experimental ones described in the literature. In their recent articles A. Imine et al. have shown that many OT implementations contain mistakes and do not possess claimed consistency properties.The present work describes an experimental library which is based on SSReflect/Coq and contains several operational transformation algorithms and proofs of their correctness.

We axiomatize hereditarily finite sets in constructive type theory and show that all models of the axiomatization are isomorphic. The axiomatization takes the empty set and adjunction as primitives and comes with a strong induction principle. Based on the axiomatization, we construct the set operations of ZF and develop the basic theory of finite ordinals and cardinality. We construct a model of the axiomatization as a quotient of an inductive type of binary trees. The development is carried out in Coq.

We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, and a faster but approximative version.To this end, we mechanize several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain. We moreover formalize algorithms for factorization of integer polynomials: Newton interpolation, factorization over the integers, and Kronecker’s factorization algorithm, as well as a factorization oracle via Berlekamp’s algorithm with the Hensel lifting.

Modular datatypes can be given a direct encoding in Coq using Church-style encodings, but this makes inductive reasoning generally problematic. We show how Mendler-style induction can be used to supplement existing techniques in modular inductive reasoning, and we present a novel technique to apply Mendler-style induction in presence of dependent induction. This results in type-based, conventional-looking proofs that take better advantage of existing Coq tactics and depend less pervasively on general semantic conditions, reducing the need for boilerplate.

Timed automata are a widely used formalism for modeling real-time systems, which is employed in a class of successful model checkers such as UPPAAL. These tools can be understood as trust-multipliers: we trust their correctness to deduce trust in the safety of systems checked by these tools. However, mistakes have previously been made. This particularly regards an approximation operation, which is used by model-checking algorithms to obtain a finite search space. The use of this operation left a soundness problem in the tools employing it, which was only discovered years after the first model checkers were devised. This work aims to provide certainty to our knowledge of the basic theory via formalization in Isabelle/HOL: we define the main concepts, formalize the classic decidability result for the language emptiness problem, prove correctness of the basic forward analysis operations, and finally outline how both streams of work can be combined to show that forward analysis with the common approximation operation correctly decides emptiness for the class of diagonal-free timed automata.

We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle/HOL, and applied it to several formalization projects in mathematics and computer science, demonstrating the high level of automation it can provide in a variety of possible proof tasks.

ITPs use names for proved theorems. Good names are either widely known or descriptive, corresponding to a theorem’s statement. Good names should be consistent with conventions, and be easy to remember. But thinking of names like this for every intermediate result is a burden: some developers avoid this by using consecutive integers or random hashes instead. We ask: is it possible to relieve the naming burden and automatically suggest sensible theorem names? We present a method to do this. It works by learning associations between existing theorem names in a large library and the names of defined objects and term patterns occurring in their corresponding statements.

We present an extension of a Coq library for relation algebras, where we provide support for cardinals in a point-free way. This makes it possible to reason purely algebraically, which is well-suited for mechanisation. We discuss several applications in the area of graph theory and program verification.

We formalise two semantics observing the expected running time of pGCL programs. The first semantics is a denotational semantics providing a direct computation of the running time, similar to the weakest pre-expectation transformer. The second semantics interprets a pGCL program in terms of a Markov decision process (MDPs), i.e. it provides an operational semantics. Finally we show the equivalence of both running time semantics.We want to use this work to implement a program logic in Isabelle/HOL to verify the expected running time of pGCL programs. We base it on recent work by Kaminski, Katoen, Matheja, and Olmedo. We also formalise the expected running time for a simple symmetric random walk discovering a flaw in the original proof.

Fourier transform based techniques are widely used for solving differential equations and to perform the frequency response analysis of signals in many safety-critical systems. To perform the formal analysis of these systems, we present a formalization of Fourier transform using higher-order logic. In particular, we use the HOL-Light’s differential, integral, transcendental and topological theories of multivariable calculus to formally define Fourier transform and reason about the correctness of its classical properties, such as existence, linearity, frequency shifting, modulation, time reversal and differentiation in time-domain. In order to demonstrate the practical effectiveness of the proposed formalization, we use it to formally verify the frequency response of an automobile suspension system.

In this paper we present CoqPIE(CoqPIE is available for download at http://github.com/kendroe/CoqPIE), a new development environment for Coq which delivers editing functionality centered around common prover usage workflow not found in existing tools. The main contributions of CoqPIE build from having an integrated parser for both Coq source and for prover output. The primary novelty is not the parser but how it is used: CoqPIE includes tools to carry out complex editing functions such as lemma extraction and replay. In proof replay for example both new and old outputs of the proof script are parsed into ASTs. These ASTs allow replay to do updates such as fixing hypothesis references.