Joe Leslie-Hurd's Bibliography

Theorem provers are now playing an important role in two diverse fields: computer system verification and mathematics. In computer system verification, they are a key component in toolsets that rigorously establish the absence of errors in critical computer hardware and software, such as processor design and safety-critical software, where traditional testing techniques provide inadequate assurance. In mathematics, they are used to check the veracity of recent high-profile proofs, such as the Four Colour Theorem and the Kepler Conjecture, whose scale and complexity have pushed traditional peer review to its limits.

In this chapter we present a project to integrate interactive and automated theorem proving. Its aim is to combine the advantages of the two paradigms. We focus on one particular application domain, which is deduction for the purpose of software verification. Some of the reported facts may not be valid in other domains. We report on the integration concepts and on the experimental results with a prototype implementation.

According to one common view, information security comes down to technical measures. Given better access control policy models, formal proofs of cryptographic protocols, approved firewalls, better ways of detecting intrusions and malicious code, and better tools for system evaluation and assurance, the problems can be solved. The author puts forward a contrary view: information insecurity is at least as much due to perverse incentives. Many of the problems can be explained more clearly and convincingly using the language of microeconomics: network externalities, asymmetric information, moral hazard, adverse selection, liability dumping and the tragedy of the commons.

The cut elimination theorem for predicate calculus states that every proof may be replaced by one which does not involve use of the cut rule. This theorem no longer holds when the system is extended with Peano's axioms to give a formalisation for arithmetic. The problem of generalisation results, since arbitrary formulae can be cut in. This makes theorem-proving very difficult - one solution is to embed arithmetic in a stronger system, where cut elimination holds. This paper describes a system based on the omega rule, and shows that certain statements are provable in this system which are not provable in Peano arithmetic without cut. Moreover, an important application is presented in the form of a new method of generalisation by means of "guiding proofs" in the stronger system, which sometimes succeeds in producing proofs in the original system when other methods fail. The implementation of such a system is also described.

Symbolic model checking has become a successful technique for verifying large finite state systems up to more than 10²0 states. The key idea of this method is that extremely large sets can often be efficiently represented with propositional formulas. Most tools implement these formulas by means of binary decision diagrams (BDDs), which have therefore become a key data structure in modern VLSI CAD systems.

Some board games like American checkers have a state space whose size is well within the range of state space sizes that have been tackled by symbolic model checking. Moreover, the question whether there is a winning strategy in these games can be reduced to two simple μ-calculus formulas. Hence, the entire problem to solve such games can be reduced to simple μ-calculus model checking problems.

In this paper, we show how to model American checkers as a finite state system by means of BDDs. We moreover specify the existence of winning strategies for both players by simple μ-calculus formulas. Further still, we report on our experimental results with our own model checking tool, and we describe some powerful improvements that we have found in trying to solve the game.

This handbook provides ready access to all of the major concepts, techniques, problems, and solutions in the emerging field of pseudorandom pattern testing. Until now, the literature in this area has been widely scattered, and published work, written by professionals in several disciplines, has treated notation and mathematics in ways that vary from source to source. This book opens with a clear description of the shortcomings of conventional testing as applied to complex digital circuits, revewing by comparison the principles of design for testability of more advanced digital technology. Offers in-depth discussions of test sequence generation and response data compression, including pseudorandom sequence generators; the mathematics of shift-register sequences and their potential for built-in testing. Also details random and memory testing and the problems of assessing the efficiency of such tests, and the limitations and practical concerns of built-in testing.

A new unification algorithm is introduced, which (unlike previous algorithms for unification in lambda-calculus) shares the pleasant properties of first-order unification. Proofs of these properties are given, in particular uniqueness of the answer and the most-general-unifier property. This unification algorithm can be used to generalize first-order proof-search algorithms to second-order logic, making possible for example a straighforward treatment of McCarthy's circumscription schema.

This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results confirm the effectiveness of the compression scheme.

This paper presents algorithms for root-finding and factorization, two problems in finite fields. The latter problem is reduced to the root-finding problem, for which a probabilistic algorithm is given. This paper is a precursor of Rabin (1980).

In this paper we consider the problem of formally verifying hardware that is specified to compute reciprocal, reciprocal square root, and power-of-two functions on floating point numbers to within a given relative error. Such specifications differ from the common case in which any given input is specified to have exactly one correct output. Our approach is based on symbolic simulation with binary decision diagrams, and involves two distinct steps. First, we prove a lemma that reduces the relative error specification to several inequalities that involve reasoning about natural numbers only. The most complex of these inequalities asserts that the product of several naturals is less-than/greater-than another natural. Second, we invoke one of several customized algorithms that decides the inequality, without performing the expensive symbolic multiplications directly. We demonstrate the effectiveness of our approach on a next-generation Intel processor design and report encouraging time and space metrics for these proofs.

This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, struct and union types, C loops and structured switch statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.

General purpose theorem provers provide advanced facilities for proving properties about specifications, and may therefore be a valuable tool in formal program development. However, these provers generally lack many of the useful structuring mechanisms found in functional programming or specification languages. This paper presents a constructive approach to adding theory morphisms and parametrisation to theorem provers, while preserving the proof support and consistency of the prover. The approach is implemented in Isabelle and illustrated by examples of an algorithm design rule and of the modular development of computational effects for imperative language features based on monads.

Abstract interpretation is a formal method that enables the static and automatic determination of run-time properties of programs. This method uses a characterization of program invariants as least and greatest fixed points of continuous functions over complete lattices of program properties. In this paper, we study precise and efficient chaotic iteration strategies for computing such fixed points when lattices are of infinite height and speedup techniques, known as widening and narrowing, have to be used. These strategies are based on a weak topological ordering of the dependency graph of the system of semantic equations associated with the program and minimize the loss in precision due to the use of widening operators. We discuss complexity and implementation issues and give precise upper bounds on the complexity of the intraprocedural and interprocedural abstract interpretation of higher-order programs based on the structure of their control flow graph.

Ordered Binary-Decision Diagrams (OBDDs) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and equivalence straightforward. A number of operations on Boolean functions can be implemented as graph algorithms on OBDD data structures. Using OBDDs, a wide variety of problems can be solved through symbolic analysis. First, the possible variations in system parameters and operating conditions are encoded with Boolean variables. Then the system is evaluated for all variations by a sequence of OBDD operations. Researchers have thus solved a number of problems in digital-system design, finite-state system analysis, artificial intelligence, and mathematical logic. This paper describes the OBDD data structure and surveys a number of applications that have been solved by OBDD-based symbolic analysis.

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most of the protocols found in the literature contain redundancies or security flaws. A simple logic has allowed us to describe the beliefs of trustworthy parties involved in authentication protocols and the evolution of these beliefs as a consequence of communication. We have been able to explain a variety of authentication protocols formally, to discover subtleties and errors in them, and to suggest improvements. In this paper we present the logic and then give the results of our analysis of four published protocols, chosen either because of their practical importance or because they serve to illustrate our method.

Previous symbolic software model checkers (i.e., program analysis tools based on predicate abstraction, pushdown model checking and iterative counterexample-guided abstraction refinement, etc.) are restricted to safety properties. Terminator is the first software model checker for termination. It is now being used to prove that device driver dispatch routines always return to their caller (or return counterexamples if they if they fail to terminate).

The quality of a programming language itself is only one component in the ability of application writers to get the job done. Programming languages can succeed or fail based on the breadth and quality of their library collection. Over the last few years, the Haskell community has risen to the task of building the library infrastructure necessary for Haskell to succeed as a programming language suitable for writing real-world applications. This on-going work, the Cabal and Hackage effort, is built on the open source model of distributed development, and have resulted in a flowering of development in the language with more code produced and reused now than at any point in the community's history. It is easier to obtain and use Haskell code, in a wider range of environments, than ever before. This demonstration describes the infrastructure and process of Haskell development inside the Cabal/Hackage framework, including the build system, library dependency resolution, centralised publication, documentation and distribution, and how the code escapes outward into the wider software community. We survey the benefits and trade-offs in a distributed, collaborative development ecosystem and look at a proposed Haskell Platform that envisages a complete Haskell development environment, batteries included.

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.

In many instances of fixed-point multiplication, a full precision result is not required. Instead it is sufficient to return a faithfully rounded result. Faithful rounding permits the machine representable number either immediately above or below the full precision result, if the latter is not exactly representable. Multipliers which take full advantage of this freedom can be implemented using less circuit area and consuming less power. The most common implementations internally truncate the partial product array. However, truncation applied to the most common of multiplier architectures, namely Booth architectures, results in non-commutative implementations. The industrial adoption of truncated multipliers is limited by the absence of formal verification of such implementations, since exhaustive simulation is typically infeasible. We present a commutative truncated Booth multiplier architecture and derive closed form necessary and sufficient conditions for faithful rounding. We also provide the bit-vectors giving rise to the worst-case error. We present a formal verification methodology based on ACL2 which scales up to 42 bit multipliers. We synthesize a range of commutative faithfully rounded multipliers and show that truncated booth implementations are up to 31% smaller than externally truncated multipliers.

Keywords: sufficient conditions;systematics;commutation;computer architecture;digital arithmetic;formal verification

In this paper symbolic exploration with binary decision diagrams (BDDs) is applied to two-player games to improve main memory consumption for reachability analysis and game-theoretical classification, since BDDs provide a compact representation for large set of game positions. A number of examples are evaluated: Tic-Tac-Toe, Nim, Hex, and Four Connect. In Chess we restrict the considerations to the creation of endgame databases. The results are preliminary, but the study puts forth the idea that BDDs are widely applicable in game playing and provides a universal tool for people interested in quickly solving practical problems.

IMPS is an Interactive Mathematical Proof System intended as a general purpose tool for formulating and applying mathematics in a familiar fashion. The logic of IMPS is based on a version of simple type theory with partial functions and subtypes. Mathematical specification and inference are performed relative to axiomatic theories, which can be related to one another via inclusion and theory interpretation. IMPS provides relatively large primitive inference steps to facilitate human control of the deductive process and human comprehension of the resulting proofs. An initial theory library containing almost a thousand repeatable proofs covers significant portions of logic, algebra and analysis, and provides some support for modeling applications in computer science.

Simple type theory, also known as higher-order logic, is a natural extension of first-order logic which is simple, elegant, highly expressive, and practical. This paper surveys the virtues of simple type theory and attempts to show that simple type theory is an attractive alternative to first-order logic for practical-minded scientists, engineers, and mathematicians. It recommends that simple type theory be incorporated into introductory logic courses offered by mathematics departments and into the undergraduate curricula for computer science and software engineering students.

We present a generic digit serial method (DSM) to compute the digits of a real number V. Bounds on these digits, and on the errors in the associated estimates of V formed from these digits, are derived. To illustrate our results, we derive bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable hardware designers to determine, for example, whether a given choice of DSM parameters allows rapid formation and rounding of approximations to V.

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

Android is a popular mobile-device platform developed by Google. Android's application model is designed to encourage applications to share their code and data with other applications. While such sharing can be tightly controlled with permissions, in general users cannot determine what applications will do with their data, and thereby cannot decide what permissions such applications should run with. In this paper we present SCanDroid, a tool for reasoning automatically about the security of Android applications. SCanDroid's analysis is modular to allow incremental checking of applications as they are installed on an Android device. It extracts security specifications from manifests that accompany such applications, and checks whether data flows through those applications are consistent with those specifications. To our knowledge, SCanDroid is the first program analysis tool for Android, and we expect it to be useful for automated security certification of Android applications.

An algorithm is presented which eliminates second–order quantifiers over predicate variables in formulae of type exists P1,...,PnF where F is an arbitrary formula of first–order predicate logic. The resulting formula is equivalent to the original formula – if the algorithm terminates. The algorithm can for example be applied to do interpolation, to eliminate the second–order quantifiers in circumscription, to compute the correlations between structures and power structures, to compute semantic properties corresponding to Hilbert axioms in non classical logics and to compute model theoretic semantics for new logics.

This report gives an account of a successful formalization of the proof of the Four Colour Theorem, which was fully checked by the Coq v7.3.1 proof assistant. This proof is largely based on the mixed mathematics/computer proof of Robertson et al, but contains original contributions as well. This document is organized as follows: section 1 gives a historical introduction to the problem and positions our work in this setting; section 2 defines more precisely what was proved; section 3 explains the broad outline of the proof; section 4 explains how we exploited the features of the Coq assistant to conduct the proof, and gives a brief description of the tactic shell that we used to write our proof scripts; section 5 is a detailed account of the formal proof (for even more details the actual scripts can be consulted); section 6 is a chronological account of how the formal proof was developed; finally, we draw some general conclusions in section 7.

Set theory is the standard foundation for mathematics, but the majority of general purpose mechanized proof assistants support versions of type theory (higher order logic). Examples include Alf, Automath, Coq, Ehdm, HOL, IMPS, Lambda, LEGO, Nuprl, PVS and Veritas. For many applications type theory works well and provides, for specification, the benefits of type-checking that are well-known in programming. However, there are areas where types get in the way or seem unmotivated. Furthermore, most people with a scientific or engineering background already know set theory, whereas type theory may appear inaccessable and so be an obstacle to the uptake of proof assistants based on it. This paper describes some experiments (using HOL) in combining set theory and type theory; the aim is to get the best of both worlds in a single system. Three approaches have been tried, all based on an axiomatically specified type V of ZF-like sets: (i) HOL is used without any additions besides V; (ii) an embedding of the HOL logic into V is provided; (iii) HOL axiomatic theories are automatically translated into set-theoretic definitional theories. These approaches are illustrated with two examples: the construction of lists and a simple lemma in group theory.

During the first week of July 1995 I visited SRI Menlo Park to find out more about PVS (Prototype Verification System). The preceding week I attended LICS95, where I had several talks with Natarajan Shankar accompanied by demos of the system on his SparcBook laptop. This note consists of a somewhat rambling and selective report on some of the things I learned, together with a discussion of their implications for the evolution of the HOL system.

Two methods of programming BDD-based symbolic algorithms in the Hol98 proof assistant are presented. The goal is to provide a platform for implementing intimate combinations of deduction and algorithmic verification, like model checking. The first programming method uses a small kernel of ML functions to convert between BDDs, terms and theorems. It is easy to use and is suitable for rapid prototying experiments. The second method requires lower-level programming but can support more efficient calculations. It is based on an LCF-like use of an abstract type to encapsulate rules for manipulating judgements r t -> b meaning “logical term t is represented by BDD b with respect to variable order r”. The two methods are illustrated by showing how to perform the standard fixed-point calculation of the BDD of the set of reachable states of a finite state machine.

A generalisation of Milner's `LCF approach' is described. This allows algorithms based on binary decision diagrams (BDDs) to be programmed as derived proof rules in a calculus of representation judgements. The derivation of representation judgements becomes an LCF-style proof by defining an abstract type for judgements analogous to the LCF type of theorems. The primitive inference rules for representation judgements correspond to the operations provided by an efficient BDD package coded in C (BuDDy). Proof can combine traditional inference with steps inferring representation judgements. The resulting system provides a platform to support a tight and principled integration of theorem proving and model checking. The methods are illustrated by using them to solve all instances of a generalised Missionaries and Cannibals problem.

The Accellera Property Specification Language (PSL) is designed for the formal specification of hardware. The Reference Manual contains a formal semantics, which we previously encoded in a machine readable version of higher order logic. In this paper we describe how to `execute' the formal semantics using proof scripts coded in the HOL theorem prover's metalanguage ML. The goal is to see if it is feasible to implement useful tools that work directly from the official semantics by mechanised proof. Such tools will have a high assurance of conforming to the standard. We have implemented two experimental tools: an interpreter that evaluates whether a finite trace w, which may be generated by a simulator, satisfies a PSL formula f (i.e. w ⊨f), and a compiler that converts PSL formulas to checkers in an intermediate format suitable for translation to HDL for inclusion in simulation test-benches. Although our tools use logical deduction and are thus slower than hand-crafted implementations, they may be speedy enough for some applications. They can also provide a reference for more efficient implementations.

This work reports on the author's experience designing, implementing, and formally verifying a low-level piece of system software. The timing model and the adaptation of an existing information flow policy to a monadic framework are reasonably novel. Interactive compilation through equational rewriting worked well in practice. Finally, the project uncovered some potential areas for improving interactive theorem provers.

We present two tools which together allow reasoning about (a substantial subset of) Haskell programs. One is the code generator of the proof assistant Isabelle, which turns specifications formulated in Isabelle's higher-order logic into executable Haskell source text; the other is Haskabelle, a tool to translate programs written in Haskell into Isabelle specifications. The translation from Isabelle to Haskell directly benefits from the rigorous correctness approach of a proof assistant: generated Haskell programs are always partially correct w.r.t. to the specification from which they are generated.

This book presents a systestematic treatment of deductive aspects and structures of fuzzy logic understood as many valued logic sui generis. Some important systems of real-valued propositional and predicate calculus are defined and investigated. The aim is to show that fuzzy logic as a logic of imprecise (vague) propositions does have well-developed formal foundations and that most things usually named `fuzzy inference' can be naturally understood as logical deduction.

There are two main groups of intended readers. First, logicians: they can see that fuzzy logic is indeed a branch of logic and may find several very interesting open problems. Second, equally important, researchers involved in fuzzy logic applications and soft computing. As a matter of fact, most of these are not professional logicians so that it can easily happen that an application, clever and successful as it may be, is presented in a way which is logically not entirely correct or may appear simple-minded. (Standard presentations of the logical aspects of fuzzy controllers are the most typical example.) This fact would not be very important if only the bon ton of logicians were harmed; but it is the opinion of the author (who is a mathematical logician) that a better understanding of the strictly logical basis of fuzzy logic (in the usual broad sense) is very useful for fuzzy logic appliers since if they know better what they are doing, they may hope to do it better. In addition, a better mutual understanding between (classical) logicians and researchers in fuzzy logic, promises to lead to deeper cooperation and new results.

Audience: mathematicians, logicians, computer scientists, specialists in artificial intelligence and knowledge engineering, developers of fuzzy logic.

This article gives an introduction to a long-term project called Flyspeck, whose purpose is to give a formal verification of the Kepler Conjecture. The Kepler Conjecture asserts that the density of a packing of equal radius balls in three dimensions cannot exceed pi/sqrt18. The original proof of the Kepler Conjecture, from 1998, relies extensively on computer calculations. Because the proof relies on relatively few external results, it is a natural choice for a formalization effort.

We consider two approaches to giving semantics to first-order logics of probability. The first approach puts a probability on the domain, and is appropriate for giving semantics to formulas involving statistical information such as “The probability that a randomly chosen bird flies is greater than .9.” The second approach puts a probability on possible worlds, and is appropriate for giving semantics to formulas describing degrees of belief, such as “The probability that Tweety (a particular bird) flies is greater than .9.” We show that the two approaches can be easily combined, allowing us to reason in a straightforward way about statistical information and degrees of belief. We then consider axiomatizing these logics. In general, it can be shown that no complete axiomatization is possible. We provide axiom systems that are sound and complete in cases where a complete axiomatization is possible, showing that they do allow us to capture a great deal of interesting reasoning about probability.

"One of the key papers in non-separable theory. [To show that f IN measurable E U implies countable range] One may use Section 2, Corollary 7, with the observation that [0,1] satisfies the assumptions and, in your situation, the collection f^(-1)(x), x∈X is even completely additive-Borel"

One way to ensure correctness of the inference performed by computer theorem provers is to force all proofs to be done step by step in a simple, more or less traditional, deductive system. Using techniques pioneered in Edinburgh LCF, this can be made palatable. However, some believe such an approach will never be efficient enough for large, complex proofs. One alternative, commonly called reflection, is to analyze proofs using a second layer of logic, a metalogic, and so justify abbreviating or simplifying proofs, making the kinds of shortcuts humans often do or appealing to specialized decision algorithms. In this paper we contrast the fully-expansive LCF approach with the use of reflection. We put forward arguments to suggest that the inadequacy of the LCF approach has not been adequately demonstrated, and neither has the practical utility of reflection (notwithstanding its undoubted intellectual interest). The LCF system with which we are most concerned is the HOL proof assistant.

The plan of the paper is as follows. We examine ways of providing user extensibility for theorem provers, which naturally places the LCF and reflective approaches in opposition. A detailed introduction to LCF is provided, emphasizing ways in which it can be made efficient. Next, we present a short introduction to metatheory and its usefulness, and, starting from Gödel's proofs and Feferman's transfinite progressions of theories, look at logical `reflection principles'. We show how to introduce computational `reflection principles' which do not extend the power of the logic, but may make deductions in it more efficient, and speculate about their practical usefulness. Applications or proposed applications of computational reflection in theorem proving are surveyed, following which we draw some conclusions. In an appendix, we attempt to clarify a couple of other notions of `reflection' often encountered in the literature.

The paper questions the too-easy acceptance of reflection principles as a practical necessity. However I hope it also serves as an adequate introduction to the concepts involved in reflection and a survey of relevant work. To this end, a rather extensive bibliography is provided.

Binary Decision Diagrams (BDDs) are a representation for Boolean formulas which makes many operations, in particular tautology-checking, surprisingly efficient in important practical cases. In contrast to such custom decision procedures, the HOL theorem prover expands all proofs out to a sequence of extremely simple primitive inferences. In this paper we describe how the BDD algorithm may be adapted to comply with such strictures, helping us to understand the strengths and limitations of the HOL approach.

Many implementations of model elimination perform proof search by iteratively increasing a bound on the total size of the proof. We propose an optimized version of this search mode using a simple divide-and-conquer refinement. Optimized and unoptimized modes are compared, together with depth-bounded and best-first search, over the entire TPTP problem library. The optimized size-bounded mode seems to be the overall winner, but for each strategy there are problems on which it performs best. Some attempt is made to analyze why. We emphasize that our optimization, and other implementation techniques like caching, are rather general: they are not dependent on the details of model elimination, or even that the search is concerned with theorem proving. As such, we believe that this study is a useful complement to research on extending the model elimination calculus.

It is generally accepted that in principle it's possible to formalize completely almost all of present-day mathematics. The practicability of actually doing so is widely doubted, as is the value of the result. But in the computer age we believe that such formalization is possible and desirable. In contrast to the QED Manifesto however, we do not offer polemics in support of such a project. We merely try to place the formalization of mathematics in its historical perspective, as well as looking at existing praxis and identifying what we regard as the most interesting issues, theoretical and practical.

The HOL theorem prover is implemented in the LCF style, meaning that all inference is ultimately reduced to a collection of very simple (forward) primitive inference rules. By programming it is possible to build alternative means of proving theorems on top, while preserving security. Existing HOL proofs styles are, however, very different from those used in textbooks. Here we describe the addition of another proof style, inspired by Mizar. We believe the resulting system combines some of the best features of both HOL and Mizar.

We are concerned with how computer theorem provers should expect users to communicate proofs to them. There are many stylistic choices that still allow the machine to generate a completely formal proof object. The most obvious choice is the amount of guidance required from the user, or from the machine perspective, the degree of automation provided. But another important consideration, which we consider particularly significant, is the bias towards a `procedural' or `declarative' proof style. We will explore this choice in depth, and discuss the strengths and weaknesses of declarative and procedural styles for proofs in pure mathematics and for verification applications. We conclude with a brief summary of our own experiments in trying to combine both approaches.

HOL Light is a new version of the HOL theorem prover. While retaining the reliability and programmability of earlier versions, it is more elegant, lightweight, powerful and automatic; it will be the basis for the Cambridge component of the HOL-2000 initiative to develop the next generation of HOL theorem provers. HOL Light is written in CAML Light, and so will run well even on small machines, e.g. PCs and Macintoshes with a few megabytes of RAM. This is in stark contrast to the resource-hungry systems which are the norm in this field, other versions of HOL included. Among the new features of this version are a powerful simplifier, effective first order automation, simple higher-order matching and very general support for inductive and recursive definitions.

Many theorem provers, model checkers and other hardware verification tools are tied to a particular set of facilities and a particular style of interaction. However HOL Light offers a wide range of proof tools and proof styles to suit the needs of various applications. For work in high-level mathematical theories, one can use a more `declarative' textbook-like style of proof (inspired by Trybulec's Mizar system). For larger but more routine and mechanical applications, HOL Light includes more `procedural' automated tools for simplifying complicated expressions, proving large tautologies etc. We believe this unusual range makes HOL Light a particularly promising vehicle for floating point verification, which involves a mix of abstract mathematics and concrete low-level reasoning. We will aim to give a brief tutorial introduction to the system, illustrating some of its features by way of such floating point verification examples. In this paper we explain the system and its possible applications in a little more detail.

We describe the computer formalization of a complex-analytic proof of the Prime Number Theorem (PNT), a classic result from number theory characterizing the asymptotic density of the primes. The formalization, conducted using the HOL Light theorem prover, proceeds from the most basic axioms for mathematics yet builds from that foundation to develop the necessary analytic machinery including Cauchy’s integral formula, so that we are able to formalize a direct, modern and elegant proof instead of the more involved ‘elementary’ Erdös-Selberg argument. As well as setting the work in context and describing the highlights of the formalization, we analyze the relationship between the formal proof and its informal counterpart and so attempt to derive some general lessons about the formalization of mathematics.

Endgame databases have become an integral part of modern chess programs during the past few years. Since the early 1990s two different kinds of endgame databases are publicly available, namely Edwards' so-called "tablebases" and Thompson's collection of 5-piece databases. Although Thompson's databases enjoy much wider international fame, most current chess programs use tablebases because they integrate far better with the rest of the search. For the benefit of all those enthusi- asts who intend to incorporate endgame databases into their own chess programs, this article describes the index schemes of Edwards' tablebases and Thompson's databases in detail, explains their differences, and provides a comparative evaluation of both.

In addition we introduce new indexing methods that improve on the published state-of-the-art and shrink the respective index ranges even further (especially for large databases and endgames with Pawns). This reduces the overall space requirements of the resulting databases substantially. We also propose several solutions for the problem of potential en-passant captures in endgame databases with at least one Pawn per each side. Shortly after the initial submission of our original text, Nalimov independently applied similar techniques as ours and even more advanced index schemes to his new tablebases which are now publicly available on the Internet, too. We briefly put his work into perspective as well.

A description of the hol98 reals library, ported partly from the reals library in HOL90 and partly from the real library in hol-light.

Gandalf is a first-order resolution theorem-prover, optimized for speed and specializing in manipulations of large clauses. In this paper I describe GANDALF_TAC, a HOL tactic that proves goals by calling Gandalf and mirroring the resulting proofs in HOL. This call can occur over a network, and a Gandalf server may be set up servicing multiple HOL clients. In addition, the translation of the Gandalf proof into HOL fits in with the LCF model and guarantees logical consistency.

There are many algorithms that make use of probabilistic choice, but a lack of tools available to specify and verify their operation. The primary contribution of this paper is a lightweight modelling of such algorithms in higher-order logic, together with some key properties that enable verification. The theory is applied to a uniform random number generator and some basic properties are established. As a secondary contribution, all the theory developed has been mechanized in the hol98 theorem-prover.

A description of the hol98 probability library.

We are improving equality reasoning in automatic theorem-provers, and congruence classes provide an efficient storage mechanism for terms, as well as the congruence closure decision procedure. We describe the technical steps involved in integrating logic variables with congruence classes, and present an algorithm that can be proved to find all matches between classes (modulo certain equalities). An application of this algorithm makes possible a percolation algorithm for undirected rewriting in minimal space; this is described and an implementation in hol98 is examined in some detail.

We show how PVS-style predicate subtyping can be simulated in HOL using predicate sets, and explain how to perform subtype checking using this model. We illustrate some applications of this to specification and verification in HOL, and also demonstrate some limits of the approach. Finally we show preliminary results of a subtype checker that has been integrated into a contextual rewriter.

This thesis shows how probabilistic algorithms can be formally verified using a mechanical theorem prover.

We begin with an extensive foundational development of probability, creating a higher-order logic formalization of mathematical measure theory. This allows the definition of the probability space we use to model a random bit generator, which informally is a stream of coin-flips, or technically an infinite sequence of IID Bernoulli(1/2) random variables.

Probabilistic programs are modelled using the state-transformer monad familiar from functional programming, where the random bit generator is passed around in the computation. Functions remove random bits from the generator to perform their calculation, and then pass back the changed random bit generator with the result.

Our probability space modelling the random bit generator allows us to give precise probabilistic specifications of such programs, and then verify them in the theorem prover.

We also develop technical support designed to expedite verification: probabilistic quantifiers; a compositional property subsuming measurability and independence; a probabilistic while loop together with a formal concept of termination with probability 1. We also introduce a technique for reducing properties of a probabilistic while loop to properties of programs that are guaranteed to terminate: these can then be established using induction and standard methods of program correctness.

We demonstrate the formal framework with some example probabilistic programs: sampling algorithms for four probability distributions; some optimal procedures for generating dice rolls from coin flips; the symmetric simple random walk. In addition, we verify the Miller-Rabin primality test, a well-known and commercially used probabilistic algorithm. Our fundamental perspective allows us to define a version with strong properties, which we can execute in the logic to prove compositeness of numbers.

We present a probabilistic version of the while loop, in the context of our mechanized framework for verifying probabilistic programs. The while loop preserves useful program properties of measurability and independence, provided a certain condition is met. This condition is naturally interpreted as “from every starting state, the while loop will terminate with probability 1”, and we compare it to other probabilistic termination conditions in the literature. For illustration, we verify in HOL two example probabilistic algorithms that necessarily rely on probabilistic termination: an algorithm to sample the Bernoulli(p) distribution using coin-flips; and the symmetric simple random walk.

The focus of this paper is the question: “How suited is the HOL theorem prover to the verification of probabilistic programs?” To answer this, we give a brief introduction to our model of probabilistic programs in HOL, and then compare this approach to other formal tools that have been used to verify probabilistic programs: the Prism model checker, the Coq theorem prover, and the B method.

Using the HOL theorem prover, we apply our formalization of probability theory to specify and verify the Miller-Rabin probabilistic primality test. The version of the test commonly found in algorithm textbooks implicitly accepts probabilistic termination, but our own verified implementation satisfies the stronger property of guaranteed termination. Completing the proof of correctness requires a significant body of group theory and computational number theory to be formalized in the theorem prover. Once verified, the primality test can either be executed in the logic (using rewriting) and used to prove the compositeness of numbers, or manually extracted to Standard ML and used to find highly probable primes.

In this paper we show how linear inequalities can be used to approximate Knuth-Bendix term ordering constraints, and how term operations such as substitution can be carried out on systems of inequalities. Using this representation allows an off-the-shelf linear arithmetic decision procedure to check the satisfiability of a set of ordering constraints. We present a formal description of a resolution calculus where systems of inequalities are used to constrain clauses, and implement this using the Omega test as a satisfiability checker. We give the results of an experiment over problems in the TPTP archive, comparing the practical performance of the resolution calculus with and without inherited inequality constraints.

In this paper we evaluate the effectiveness of first-order proof procedures when used as tactics for proving subgoals in a higher-order logic interactive theorem prover. We first motivate why such first-order proof tactics are useful, and then describe the core integrating technology: an `LCF-style' logical kernel for clausal first-order logic. This allows the choice of different logical mappings between higher-order logic and first-order logic to be used depending on the subgoal, and also enables several different first-order proof procedures to cooperate on constructing the proof. This work was carried out using the HOL4 theorem prover; we comment on the ease of transferring the technology to other higher-order logic theorem provers.

We present a framework for extracting and compiling proof tools and theories from a higher order logic theorem prover, so that the theorem prover can be used as a platform for supporting reasoning in other applications. The framework is demonstrated on a small application that uses HOL4 to find proofs of arbitrary first order logic formulas.

Chess endgame databases store the number of moves required to force checkmate for all winning positions: with such a database it is possible to play perfect chess. This paper describes a method to construct endgame databases that are formally verified to logically follow from the laws of chess. The method employs a theorem prover to model the laws of chess and ensure that the construction is correct, and also a BDD engine to compactly represent and calculate with large sets of chess positions. An implementation using the HOL4 theorem prover and the BuDDY BDD engine is able to solve all four piece pawnless endgames.

Formalizing a mathematical theory using a theorem prover is a necessary first step to proving the correctness of programs that refer to that theory in their specification. This report demonstrates how the mathematical theory of elliptic curves and their application to cryptography can be formalized in higher order logic. This formal development is mechanized using the HOL4 theorem prover, resulting in a collection of formally verified functional programs (expressed as higher order logic functions) that correctly implement the primitive operations of elliptic curve cryptography.

The probabilistic guarded-command language pGCL contains both demonic and probabilistic nondeterminism, which makes it suitable for reasoning about distributed random algorithms Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-) valued functions.

We present a mechanization of the quantitative logic for pGCL using the HOL4 theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL.

The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm.

Formalizing a mathematical theory is a necessary first step to proving the correctness of programs that refer to that theory in their specification. This paper demonstrates how the mathematical theory of elliptic curves and their application to cryptography can be formalized in higher order logic. This formal development is mechanized using the HOL4 theorem prover, resulting in a collection of higher order logic functions that correctly implement the primitive operations of elliptic curve cryptography.

This report surveys existing approaches to embedding Cryptol programs in higher order logic, and presents a new approach that aims to simplify as much as possible reasoning about the embedded programs.

TERMINATOR is a static analysis tool developed by Microsoft Research for proving termination of Windows device drivers written in C. This proof pearl describes a formalization in higher order logic of the program analysis employed by TERMINATOR, and verifies that if the analysis succeeds then program termination logically follows.

Interactive theorem proving has grown from toy examples to major projects formalizing mathematics and verifying software, and there is now a critical need for theory engineering techniques to support these efforts. This paper introduces the OpenTheory project, which aims to provide an effective package management system for logical theories. The OpenTheory article format allows higher order logic theories to be exported from one theorem prover, compressed by a stand-alone tool, and imported into a different theorem prover. Articles naturally support theory interpretations, which is the mechanism by which theories can be cleanly transferred from one theorem prover context to another, and which also leads to more efficient developments of standard theories.

SELinux security policies are powerful tools to implement properties such as process confinement and least privilege. They can also be used to support MLS policies on SELinux. However, the policies are very complex, and creating them is a difficult and error-prone process. Furthermore, it is not possible to state explicit constraints on an SELinux policy such as “information flowing to the network must be encrypted”.

We present two related Domain Specific Languages (DSL) to make it much easier to specify SELinux security policies. The first DSL is called Lobster. Lobster allows the user to state an information flow policy at a very high level of abstraction, and then refine the policy into lower and lower levels until it can be translated by the Lobster compiler into an SELinux policy. The second DSL is called Symbion. Symbion allows the user to state policy constraints such as “information flowing to the network must be encrypted”. Symbion and Lobster will then interface with tools that can check that the policy satisfies the constraints.

We also present the analysis tool Shrimp, with which we are able to analyze and find errors in the SELinux Reference Policy. Shrimp is also the basis for our ongoing effort in reverse translating the Reference Policy into Lobster.

Since Lobster and Symbion represent information flows and contraints on information flows, they are more broadly applicable than to just SELinux. We will point to some of the directions we wish to take Lobster and Symbion beyond SELinux.

The chess endgame is increasingly being seen through the lens of, and therefore effectively defined by, a data `model' of itself. It is vital that such models are clearly faithful to the reality they purport to represent. This paper examines that issue and systems engineering responses to it, using the chess endgame as the exemplar scenario. A structured survey has been carried out of the intrinsic challenges and complexity of creating endgame data by reviewing the past pattern of errors during work in progress, surfacing in publications and occurring after the data was generated. Specific measures are proposed to counter observed classes of error-risk, including a preliminary survey of techniques for using state-of-the-art verification tools to generate EGTs that are correct by construction. The approach may be applied generically beyond the game domain.

Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is effective package management, which has the potential to simplify the development of logical theories by precisely checking dependencies and promoting re-use. This paper introduces a domain-specific language for defining composable packages of higher order logic theories, which is designed to naturally handle the complex dependency structures that often arise in theory development. The package composition language functions as a module system for theories, and the paper presents a well-defined semantics for the supported operations. Preliminary tests of the package language and its toolset have been made by packaging the theories distributed with the HOL Light theorem prover. This experience is described, leading to some initial theory engineering discussion on the ideal properties of a reusable theory.

Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is cross-prover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. The core contribution of this paper is the presentation of a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.

In functional programming, a popular approach to building recursive descent parsers is to model parsers as functions, and to define higher-order functions (or combinators) that implement grammar constructions such as sequencing, choice, and repetition. Such parsers form an instance of a monad, an algebraic structure from mathematics that has proved useful for addressing a number of computational problems. The purpose of this report is to provide a step-by-step tutorial on the monadic approach to building functional parsers, and to explain some of the benefits that result from exploiting monads. No prior knowledge of parser combinators or of monads is assumed. Indeed, this report can also be viewed as a first introduction to the use of monads in programming.

This 90min tutorial covered two of the more novel aspects of the Nuprl and PVS theorem provers:

Expressive type systems. These make specifications more consise and accurate, but good automation is needed to solve proof obligations that arise during type-checking.

Support for abstract theories. These have uses in supporting mechanical proof developments, and in the domains of program specification refinement and mathematics. Key issues are whether types can be formed for classes of abstract theories and the need for automatic inference of theory interpretations.

The tutorial assumed some familiarity with HOL-like theorem provers, but did not assume familiarity with either PVS or Nuprl in particular. The issue of Nuprl's constructivity was orthogonal to the issues discussed and was therefore glossed over.

"Johnson presents an extensive survey of computational complexity classes. Of particular interest here is his discussion of randomized, probabilistic, and stochastic complexity classes."

Current best practice for high-assurance security and safety-critical software often requires the use of machine-checked rigorous mathematical techniques. Unfortunately, while there have been some notable successes, the provision of software tools that adequately support such techniques is a hard research problem, albeit one that is slowly being solved. This paper describes some contributions to this area of research and development in ICL in recent years. This research builds both on ICL’s own experiences in building and using tools to support security applications and on work carried out by the Defence Research Agency into notations and methods for program verification.

This paper describes the use of formal development methods on an industrial safety-critical application. The Z notation was used for documenting the system specification and part of the design, and the SPARK1 subset of Ada was used for coding. However, perhaps the most distinctive nature of the project lies in the amount of proof that was carried out: proofs were carried out both at the Z level-approximately 150 proofs in 500 pages-and at the SPARK code level-approximately 9,000 verification conditions generated and discharged. The project was carried out under UK Interim Defence Standards 00-55 and 00-56, which require the use of formal methods on safety-critical applications. It is believed to be the first to be completed against the rigorous demands of the 1991 version of these standards. The paper includes comparisons of proof with the various types of testing employed, in terms of their efficiency at finding faults. The most striking result is that the Z proof appears to be substantially more efficient at finding faults than the most efficient testing phase. Given the importance of early fault detection, we believe this helps to show the significant benefit and practicality of large-scale proof on projects of this kind.

Complete formal verification is the only way to guarantee that a system is free of programming errors.

We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.

seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

Proof tools in interactive theorem provers are usually developed within and tied to a specific system, which leads to a duplication of effort to make the functionality available in different systems. Many verification projects would benefit from access to proof tools developed in other systems. Using OpenTheory as a language for communicating between systems, we show how to turn a proof tool implemented for one system into a standalone tactic available to many systems via the internet. This enables, for example, LCF-style proof reconstruction efforts to be shared by users of different interactive theorem provers and removes the need for each user to install the external tool being integrated.

OpenTheory is being used for the first time (in work to be described at ITP 2013) as a tool in a larger project, as opposed to in an example demonstrating OpenTheory's capability. The tool works, demonstrating its viability. But it does not work completely smoothly, because the use case is somewhat at odds with OpenTheory's primary design goals. In this extended abstract, we explore the tensions between the goals that OpenTheory-like systems might have, and question the relative importance of various kinds of use. My hope is that describing issues arising from work in progress will stimulate fruitful discussion relevant to the development of proof exchange systems.

We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, “with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2”.

The presumed difficulty of computing discrete logarithms in finite fields is the basis of several popular public key cryptosystems. The secure identification option of the Sun Network File System, for example, uses discrete logarithms in a field GF(p) with p a prime of 192 bits. This paper describes an implementation of a discrete logarithm algorithm which shows that primes of under 200 bits, such as that in the Sun system, are very insecure. Some enhancements to this system are suggested.

A method of writing proofs is proposed that makes it much harder to prove things that are not true. The method, based on hierarchical structuring, is simple and practical.

Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification languuage without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased complexity,and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verification, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages.

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the `LT' Logic Theory Machine of Newell, Shaw and Simon. In game-playing terms, the `initial position' is the core set of axioms chosen for the particular logic and the `moves' are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting `HoTT' book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

Maintaining software in the face of evolving dependencies is a challenging problem, and in addition to good release practices there is a need for automatic dependency analysis tools to avoid errors creeping in. Verified software reveals more semantic information in the form of mechanized proofs of functional specifications, and this can be used for dependency analysis. In this paper we present a scheme for automatic dependency analysis of verified software, which for each program checks that the collection of installed libraries is sufficient to guarantee its functional correctness. We illustrate the scheme with a case study of Haskell packages verified in higher order logic. The dependency analysis reduces the burden of maintaining verified Haskell packages by automatically computing version ranges for the packages they depend on, such that any combination provides the functionality required for correct operation.

As cryptography becomes more vital to the infrastructure of computing systems, it becomes increasingly vital to be able to rapidly and correctly produce new implementations of cryptographic algorithms. To address these challenges, we introduce a new, formal methods-based approach to the specification and implementation of cryptography, present a number of scenarios of use, an overview of the language, and present part of a specification of the advanced encryption standard.

We give a general goal directed method for solving the E-unification problem. Our inference system is a generalization of the inference rules for Syntactic Theories, except that our inference system is proved complete for any equational theory. We also show how to easily modify our inference system into a more restricted inference system for Syntactic Theories, and show that our completeness techniques prove completeness there also.

We give a general goal directed method for solving the -unification problem. Our inference system is a generalization of the inference rules for Syntactic Theories, except that our inference system is proved complete for any equational theory. We also show how to easily modify our inference system into a more restricted inference system for Syntactic Theories, and show that our completeness techniques prove completeness there also.

The functional programming language ML has been undergoing a thorough redesign during the past year, and the module facility described here has been proposed as part of the revised language, now called Standard ML. The design has three main goals: (1) to facilitate the structuring of large ML programs; (2) to support separate compilation and generic library units; and (3) to employ new ideas in the semantics of data types to extend the power of ML's polymorphic type system. It is based on concepts inherent in the structure of ML, primarily the notions of a declaration, its type signature, and the environment that it denotes.

Probabilistic predicate transformers guarantee standard (ordinary) predicate transformers to incorporate a notion of probabilistic choice in imperative programs. The basic theory of that, for finite state spaces, is set out in [5], together with a statements of their `healthiness conditions'. Here the earlier results are extended to infinite state spaces, and several more specialised topics are explored: the characterisation of standard and deterministic programs; and the structure of the extended space generated when `angelic choice' is added to the system.

Probabilistic choice and demonic nondeterminism have been combined in a model for sequential programs in which program refinement is defined by removing demonic nondeterminism. Here we study the more general topic of data refinement in the probabilistic setting, extending standard techniques to probabilistic programs. We use the method to obtain a quantitative assessment of safety of a (probabilistic) version of the steam boiler.

Following earlier models, we lift standard deterministic and nondeterministic semantics of imperative programs to probabilistic semantics. This semantics allows for random external inputs of known or unknown probability and random number generators. We then propose a method of analysis of programs according to this semantics, in the general framework of abstract interpretation. This method lifts an ordinary abstract lattice, for non-probabilistic programs, to one suitable for probabilistic programs. Our construction is highly generic. We discuss the influence of certain parameters on the precision of the analysis, basing ourselves on experimental results.

We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing ordinary testing, we show how to combine testing and abstract interpretation and give formulas linking the precision of the results to the number of iterations. We then discuss complexity and optimization issues and end with some experimental results.

Predicate transformers facilitate reasoning about imperative programs, including those exhibiting demonic non-deterministic choice. Probabilistic predicate transformers extend that facility to programs containing probabilistic choice, so that one can in principle determine not only whether a program is guaranteed to establish a certain result, but also its probability of doing so. We bring together independent work of Claire Jones and Jifeng He, showing how their constructions can be made to correspond; from that link between a predicate-based and a relation-based view of probabilistic execution we are able to propose "probabilistic healthiness conditions", generalising those of Dijkstra for ordinary predicate transformers. The associated calculus seems suitable for exploring further the rigorous derivation of imperative probabilistic programs.

We present a new approach for goal-directed theorem proving with equality which integrates Basic Ordered Paramodulation into a Model Elimination framework. In order to be able to use orderings and to restrict the applications of equations to non-variable positions, the goal-directed tableau construction is combined with bottom-up completion where only positive literals are overlapped. The resulting calculus thus keeps the best properties of completion while giving up only part of the goal-directedness.

The model elimination theorem prover SETHEO (version V3.3) and its equational extension E-SETHEO are presented. SETHEO employs sophisticated mechanisms of subgoal selection, elaborate iterative deepening techniques, and local failure caching methods. Its equational counterpart E-SETHEO transforms formulae containing equality (using a variant of Brand's modification method) and processes the output with the standard SETHEO system. The paper gives an overview of the theoretical background, the system architecture, and the performance of both systems.

Chess endgame tables should provide efficiently the value and depth of any required position during play. The indexing of an endgame's positions is crucial to meeting this objective. This paper updates Heinz' previous review of approaches to indexing and describes the latest approach by the first and third authors.

Heinz' and Nalimov's endgame tables (EGTs) encompass the en passant rule and have the most compact index schemes to date. Nalimov's EGTs, to the Distance-to-Mate (DTM) metric, require only 30.6 x 10^9 elements in total for all the 3-to-5-man endgames and are individually more compact than previous tables. His new index scheme has proved itself while generating the tables and in the 1999 World Computer Chess Championship where many of the top programs used the new suite of EGTs.

Higher-order patterns (HOPs) are a class of lambda-terms which behave almost like first-order terms w.r.t. unification: unification is decidable and unifiable terms have most general unifiers which are easy to compute. HOPs were first discovered by Dale Miller and subsequently developed and applied by Pfenning and Nipkow. This paper presents a stepwise development of a functional unification algorithm for HOPs. Both the usual representation of lambda-terms with alphabetic bound variables and de Bruijn's notation are treated. The appendix contains a complete listing of an implementation in Standard ML.

This article presents formalizations in higher-order logic of two proofs of Arrow’s impossibility theorem due to Geanakoplos. The Gibbard-Satterthwaite theorem is derived as a corollary. Lacunae found in the literature are discussed.

The HOL system is a mechanized proof assistant for higher-order logic that has been under continuous development since the mid-1980s, by an ever-changing group of developers and external contributors. We give a brief overview of various implementations of the HOL logic before focusing on the evolution of certain important features available in a recent implementation. We also illustrate how the module system of Standard ML provided security and modularity in the construction of the HOL kernel, as well as serving in a separate capacity as a useful representation medium for persistent, hierarchical logical theories.

We give a continuation-based implementation of rewriting for systems in the LCF tradition. These systems must construct explicit proofs of equations when rewriting, and currently do so in a way that can be very space-inefficient. An explicit representation of continuations improves performance on large terms, and on long-running computations.

We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Isabelle/HOL that have been recorded in HOL 4 or HOL-light and is therefore completely safe. Concepts in the source HOL system, that is types and constants, can be mapped to concepts in Isabelle/HOL; this facilitates a true integration of imported theorems and theorems that are already available in Isabelle/HOL. The importer is part of the standard Isabelle distribution.

Data structures and efficiency analysis for functional programming. Code in ML and Haskell. Many references.

We present methods to generate systematically the hardest test cases for multiplication, division, and square root subject to directed rounding, essentially extending previous work on number-theoretic floating-point testing to rounding modes other than to-nearest. The algorithms focus upon the rounding boundaries of the modes truncate, to-minusinfinity, and to-infinity, and programs based on them require little beyond exact arithmetic in the working precision to create billions of edge cases. We will show that the amount of work required to calculate trial multiplicands pays off in the form of free extra tests due to an interconnection among the operations considered herein. Although these tests do not replace proofs of correctness, they can be used to gain a high degree of confidence that the accuracy requirements as mandated by IEEE Standard 754 have been satisfied.

Many automatic theorem-provers rely on rewriting. Using theorems as rewrite rules helps to simplify the subgoals that arise during a proof. LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of rewriting is presented in detail. LCF provides a family of rewriting functions, and operators to combine them. A succession of functions is described, from pattern matching primitives to the rewriting tool that performs most inferences in LCF proofs. The design is highly modular. Each function performs a basic, specific task, such as recognizing a certain form of tautology. Each operator implements one method of building a rewriting function from sim- pler ones. These pieces can be put together in numerous ways, yielding a variety of rewriting strategies. The approach involves programming with higher-order functions. Rewriting functions are data val- ues, produced by computation on other rewriting functions. The code is in daily use at Cambridge, demon- strating the practical use of functional programming.

A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the flexibility to adapt to variants of set theory. Its higher-order syntax supports the definition of new binding operators. Unknowns in subgoals can be instantiated incrementally. The paper describes the derivation of rules for descriptions, relations and functions, and discusses interactive proofs of Cantor's Theorem, the Composition of Homomorphisms challenge [9], and Ramsey's Theorem [5]. A generic proof assistant can stand up against provers dedicated to particular logics.

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem to a set, such as V_ω, that is closed under Cartesian product and disjoint sum. Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schröder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions.

A verifying compiler is one that emits both object code and a proof of correspondence between object and source code. We report the use of ACL2 in building a verifying compiler for Cryptol, a stream-based language for encryption algorithm specification that targets Rockwell Collins' AAMP7 microprocessor (and is designed to compile efficiently to hardware, too). This paper reports on our success in verifying the "core" transformations of the compiler – those transformations over the sub-language of Cryptol that begin after "higher-order" aspects of the language are compiled away, and finish just before hardware or software specific transformations are exercised. The core transformations are responsible for aggressive optimizations. We have written an ACL2 macro that automatically generates both the correspondence theorems and their proofs. The compiler also supplies measure functions that ACL2 uses to automatically prove termination of Cryptol programs, including programs with mutually-recursive cliques of streams. Our verifying compiler has proved the correctness of its core transformations for multiple algorithms, including TEA, RC6, and AES. Finally, we describe an ACL2 book of primitive operations for the general specification and verification of encryption algorithms.

We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types are available.

Our embedding takes advantage of Haskell where appropriate, but we rely on no exotic features. Thus our approach translates with minimal modification to other polymorphic, typed languages such as ML and Java. Our implementation works with existing Haskell concurrency mechanisms, handles multiple communication channels and recursive session types, and infers protocols automatically.

While our implementation uses unsafe operations in Haskell, it does not violate Haskell's safety guarantees. We formalize this claim in a concurrent calculus with unsafe communication primitives over which we layer our implementation of session types, and we prove that the session types layer is safe. In particular, it enforces that channel-based communication follows consistent protocols.

The Omega test is an integer programming algorithm that can determine whether a dependence exists between two array references, and if so, under what conditions. Conventional wisdom holds that integer programming techniques are far too expensive to be used for dependence analysis, except as a method of last resort for situations that cannot be decided by simpler methods. We present evidence that suggests this wisdom is wrong, and that the Omega test is competitive with approximate algorithms used in practice and suitable for use in production compilers. The Omega test is based on an extension of Fourier-Motzkin variable elimination to integer programming, and has worst-case exponential time complexity. However, we show that for many situations in which other (polynomial) methods are accurate, the Omega test has low order polynomial time complexity. The Omega test can be used to simplify integer programming problems, rather than just deciding them. This has many applications, including accurately and efficiently computing dependence direction and distance vectors.

"This is a seminal paper on the theory of probabilistic automata. Rabin defined the notion of a language being accepted by a probabilistic automaton relative to a cutpoint lambda. One of his key results was to show that there exist finite state probabilistic automata that define non-regular languages."

Probability distributions are useful for expressing the meanings of probabilistic languages, which support formal modeling of and reasoning about uncertainty. Probability distributions form a monad, and the monadic definition leads to a simple, natural semantics for a stochastic lambda calculus, as well as simple, clean implementations of common queries. But the monadic implementation of the expectation query can be much less efficient than current best practices in probabilistic modeling. We therefore present a language of measure terms, which can not only denote discrete probability distributions but can also support the best known modeling techniques. We give a translation of stochastic lambda calculus into measure terms. Whether one translates into the probability monad or into measure terms, the results of the translations denote the same probability distribution.

The authors describe how the Crowds system works – essentially, a group of users act as web forwarders for each other in a way that appears random to outsiders. They analyse the anonymity properties of the system and compare it with other systems. Crowds enables the retrieval of information over the web with only a small amount of private information leakage to other parties.

The following list of tableaux-based theorem provers was assembled in the Spring and Summer 1993 as the result of a wide-spread enquiry via e-mail. It is intended to provide a short overview of the field and existing implementations. For each system, a short description is given. Additionally, useful information about the system is presented in tabular form. This includes the type of logic which can be handled by the system (input), the implementation language, hardware and operating systems requirements (implementation). Most of the systems are available as binaries or as sources with documentation and can be obtained via anonymous ftp or upon request. The descriptions and further information have been submitted by the individuals whose names are given as contact address. The provers are ordered alphabetically by their name (or the author's name).

Formal hardware verification has recently attracted considerable interest. The need for “correct” designs in safety-critical applications, coupled with the major cost associated with products delivered late, are two of the main factors behind this. In addition, as the complexity of the designs increase, an ever smaller percentage of the possible behaviors of the designs will be simulated. Hence, the confidence in the designs obtained by simulation is rapidly diminishing. This paper provides an introduction to the topic by describing three of the main approaches to formal hardware verification: theorem-proving, model checking and symbolic simulation. We outline the underlying theory behind each approach, we illustrate the approaches by applying them to simple examples and we discuss their strengths and weaknesses. We conclude the paper by describing current on-going work on combining the approaches to achieve multi-level verification approaches.

The development of cryptographic hardware for classified data is expensive and time consuming. We present a domain-specific language, microCryptol, and a corresponding compiler, mcc, to address these costs. microCryptol supports the capture of mathematically precise specifications of algorithms, while also allowing those specifications to be compiled to efficient imperative code able to execute on embedded microprocessors.

Attempts to use finite models to guide the search for proofs by resolution and the like in forst order logic all suffer from the need to trade off the expense of generating and maintaining models against the improvement in quality of guidance as investment in the semantic aspect of reasoning is increased. Previous attempts to resolve this tradeoff have resulted either in poor selection of models, or in fragility as the search becomes over-sensitive to the order of clauses, or in extreme slowness. Here we present a fresh approach, whereby most of the clauses for which a model is sought are treated as soft constraints. The result is a partial model of all of the clauses rather than an exact model of only a subset of them. This allows our system to combine the speed of maintaining just a single model with the robustness previously requiring multiple models. We present experimental evidence of benefits over a range of first order problem domains.

Polytypic functions have mainly been studied in the context of functional programming languages. In that setting, applications of polytypism include elegant treatments of polymorphic equality, prettyprinting, and the encoding and decoding of high-level datatypes to and from low-level binary formats. In this paper, we discuss how polytypism supports some aspects of theorem proving: automated termination proofs of recursive functions, incorporation of the results of metalanguage evaluation, and equivalence-preserving translation to a low-level format suitable for propositional methods. The approach is based on an interpretation of higher order logic types as terms, and easily deals with mutual and nested recursive types.

"This book provides a record of a conference, and contains many novel ideas for probabilistic algorithms."

Combinators, a "curried" version of lambda calculus that eliminates the need for symbol binding. Combinators can be reduced (evaluated) locally and in parallel, so they make an interesting model of parallel computation. Combinator hackers: this paper introduces some new combinators, besides S-K-I, that help keep the translation from blowing up in space.

In the last 20 years modal logic has been applied to numerous areas of computer science, including artificial intelligence, program verification, hardware verification, database theory, and distributed computing. There are two main computational problems associated with modal logic. The first problem is checking if a given formula is true in a given state of a given structure. This problem is known as the model-checking problem. The second problem is checking if a given formula is true in all states of all structures. This problem is known as the validity problem. Both problems are decidable. The model-checking problem can be solved in linear time, while the validity problem is PSPACE-complete. This is rather surprising when one considers the fact that modal logic, in spite of its apparent propositional syntax, is essentially a first-order logic, since the necessity and possibility modalities quantify over the set of possible worlds, and model checking and validity for first-order logic are computationally hard problems. Why, then, is modal logic so robustly decidable? To answer this question, we have to take a close look at modal logic as a fragment of first-order logic. A careful examination reveals that propositional modal logic can in fact be viewed as a fragment of 2-variable first-order logic. It turns out that this fragment is computationally much more tractable than full first-order logic, which provides some explanation for the tractability of modal logic. Upon a deeper examination, however, we discover that this explanation is not too satisfactory. The tractability of modal logic is quite and cannot be explained by the relationship to two-variable first-order logic. We argue that the robust decidability of modal logic can be explained by the so-called tree-model property, and we show how the tree-model property leads to automata-based decision procedures.

Category theorists invented monads in the 1960's to concisely express certain aspects of universal algebra. Functional programmers invented list comprehensions in the 1970's to concisely express certain programs involving lists. This paper shows how list comprehensions may be generalised to an arbitrary monad, and how the resulting programming feature can concisely express in a pure functional language some programs that manipulate state, handle exceptions, parse text, or invoke continuations. A new solution to the old problem of destructive array update is also presented. No knowledge of category theory is assumed.

Using program transformation techniques from the field of partial evaluation an automatic tool for generating very efficient conversions from equality-stating theorems has been implemented. In the situation where a Hol user would normally employ the built-in function GEN_REWRITE_CONV, a function that directly produces a conversion of the desired functionality, this article demonstrates how producing the conversion in the form of a program text instead of as a closure can lead to significant speed-ups. The Hol system uses a set of 31 simplifying equations on a very large number of intermediate terms derived, e.g., during backwards proofs. For this set the conversion generated by the two-step method is about twice as fast as the method currently used. When installing the new conversion, tests show that the overall running times of Hol proofs are reduced by about 10%. Apart from the speed-up this is completely invisible to the user. With cooperation from the user further speed-up is possible.

OIL, the Ontic Inference Language, is a simple bottom-up logic programming language with equality reasoning. Although intended for use in writing proof verification systems, OIL is an interesting general-purpose programming language. In some cases, very simple OIL programs can achieve an efficiency which requires a much more complicated algorithm in a traditional programming language. This thesis gives a formal semantics for OIL and some new results related to its efficient implementation. The main new result is a method of transforming bottomup logic programs with equality to bottom-up logic programs without equality. An introduction to OIL and several examples are also included.

Formal proofs generated by mechanized theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an efficient proof checker which is able to check a practical proof consisting of thousands of inference steps.

The Verilog Hardware Description Language (HDL) is defined in this standard. Verilog HDL is a formal notation intended for use in all phases of the creation of electronic systems. Because it is both machine readable and human readable, it supports the development, verification, synthesis, and testing of hardware designs; the communication of hardware design data; and the maintenance, modification, and procurement of hardware. The primary audiences for this standard are the implementors of tools supporting the language and advanced users of the language.

This standard defines a standard operating system interface and environment, including a command interpreter (or shell), and common utility programs to support applications portability at the source code level. It is the single common revision to IEEE Std 1003.1-1996, IEEE Std 1003.2-1992, and the Base Specifications of The Open Group Single UNIX Specification, Version 2.

Certification of critical software systems (e.g., for safety and security) is important to help ensure their dependability. Today, certification relies as much on evaluation of the software development process as it does on the system s properties. While the latter are preferable, the complexity of these systems usually makes them extremely difficult to evaluate. To explore these and related issues, the National Coordination Office for Information technology Research and Development asked the NRC to undertake a study to assess the current state of certification in dependable systems. The study is in two phases: the first to frame the problem and the second to assess it. This report presents a summary of a workshop held as part of the first phase. The report presents a summary of workshop participants presentations and subsequent discussion. It covers, among other things, the strengths and limitations of process; new challenges and opportunities; experience to date; organization context; and cost-effectiveness of software engineering techniques. A consensus report will be issued upon completion of the second phase.