HOL Around the World

Compiled by Sara Kalvala, University of Cambridge

This document describes briefly projects which use the HOL proof system, based on contributions from the user community. The entries are in somewhat haphazard order and classification; the intent is to provide a brief synopsis of applications and a directory for future contacts. This list is by no means comprehensive - it just contains the contributions I have received.

This list is current as of August 3, 1991. If you’d like me to add or modify something on this list, or to receive a more updated version, send me mail at sk@cl.cam.ac.uk.

1 Hardware

Traditionally, HOL has been linked to hardware verification, starting from Gordon’s initial work. From the canonical example of a multiplier, many larger circuits have been subject to verification through HOL. Many projects involve such uses of HOL, dealing however with more advanced features: timing, concurrency, and generic hardware, for example.

Applying HOL to larger and more complex designs also means that the methodology for proof had to be enhanced. The second set of projects mentions several of these.

There is also a need for integrating verification better with design methodologies. Thus another approach is to examine hardware design languages, and use and formalize information on design methodologies.

1.1 Particular Designs

Parametrized h/w: Catia Angelo (catia@imec.be).

Verification of a Mead & Conway –like alu core available in the CATHEDRAL silicon compiler environment.

SECD: Graham Birtwistle (graham@cpsc.ucalgary.ca) and Brian Graham (btg@cl.cam.ac.uk).

A full custom implementation of Landin’s SECD architecture as a microprocessor suitable for functional programming languages was specified and verified (aside from garbage collection) in HOL. The design has roughly similar complexity and size to the Viper chip.

I/O hardware: John Herbert (jmjh@cl.cam.ac.uk).

To design and verify a UART whose initial target is the VIPER, and will serve as a prototype of Transputer link verification (SAFEMOS). Specification and verification to be as general as possible so that the proofs can hopefully be reused. Fabrication will take place with XILINX user–programmable gate arrays.

Arithmetic: Shiu-Kai Chin (chin@cat.syr.edu).

HOL has been used to describe and verify several arithmetic circuit designs including word-parallel and bit-serial multipliers. These designs are parameterized with respect to interconnection structure and support general signed-binary representations.

Tamarack-3: Jeff Joyce (joyce@cs.ubc.ca).

Formal specification and verification of a very simple microprocessor featuring interrupts and asynchronous memory interface; illustrates generic specification of hardware and use of an embedded notation (namely, temporal logic).

Automata theory: Paul Loewenstein (melasv!paul@net.UU.uunet).

Used for the verification of multipliers, and single and multiprocessor cache systems.

Regulator: Roger Jones (R.B.Jones@win0103.uucp) et. al., International Computers Limited.

Formal verification of security properties of a hardware ”one way regulator”, leading to product certification as ”Exceeding the requirements of UKL6” (similar to US DoD A1).

1.2 Design Environments

Silage: Catia Angelo (catia@imec.be).

Early phases of defining the semantics of Silage, a language for DSP, in HOL. Basically, Silage describes a signal flow graph and we have the intention of using HOL to make correct transformations in Silage descriptions.

ELLA: Richard Boulton (rjb@cl.cam.ac.uk) and John Harrison (jrh@cl.cam.ac.uk).

Specification of the formal semantics of a subset of the ELLA hardware description language in HOL with theorem–proving support for reasoning about ELLA designs. Development of a methodology for adding formal methods to conventional CAD. Translate ELLA to HOL via explicit semantics and test the methodology by designing XILINX chips.

VHDL: John Van Tassel (jvt@cl.cam.ac.uk).

To define a subset of VHDL tractable for formal methods, to specify its semantics in HOL and hence to develop a set of proof tools. Build on the results and lessons of the HOL–ELLA project with the understanding that VHDL is a much more complex language.

COSMOS: Carl Seger and Jeff Joyce (joyce@cs.ubc.ca):

An approach which combines HOL with the COSMOS system (symbolic simulation of CMOS). We are currently developing the mathematical interface between HOL and COSMOS. This work involves use of compiler verification techniques to bootstrap a specification language which serves as an intermediate form between HOL and COSMOS.

CATHEDRAL-II: Wim Ploegaerts (ploegaer@imec.be).

Silicon compiler for real-time, complex decision-making signal processing applications. The generated chips perform complex arithmetic operations. As we believe software verification to be even harder than hardware verification, we will not verify the tools (and algorithms) but we will try to set up an environment for the validation of the synthesis results. The result of this work will be a library of correct hardware transformation rules (in HOL) and a guaranteed correct library in CATHEDRAL.

VLSI design: Phil Windley (windley@cheetah.cs.uidaho.edu).

Integrating HOL with a suite of VLSI design tools used for designing VLSI chips in the NASA Space Engineering Research Center for VLSI design.

VISULA: Geoff Scullard (geoff@win.icl.co.uk), International Computers Limited

HOL–VISULA link. Takes netlist output from the VISULA CAD tool and converts this into HOL.

1.3 Hardware Reasoning Methodologies

Security: Phil Windley (windley@cheetah.cs.uidaho.edu).

Designing, verifying and fabricating a microprocessor with security features.

Shared memory: Tim Leonard (leonard@eagle1.enet.dec.com).

Formal specification of computer architectures, particularly multiprocessors with shared memory. I’m representing system behavior as a partially ordered set of memory references, and am trying to produce an integrated formal model that covers shared memory, memory coherence, and synchronization.

H/w development: Claude Fleurey (fleurey@esonvmla.iinus1.ibm.com).

HOL is intended to provide us a formal frame work into which the proof of the designed hardware (micro-processors) can be conducted.

Real-time: Glenn MacEwen (macewen@qucis.queensu.ca).

The specification and verification of components of real-time distributed systems is being investigated, and a theory based on higher-order logic is being used as the formal basis for two higher level specification languages. Two major objectives of the project are to separate the concerns of external applications requirements from those of internal system design, and to bridge the gap between the formal design specification and implementation.

Hardware reasoning: Albert Camilleri (ac@hplb.hpl.hp.com) and Roger Fleming (raf@hplb.hpl.hp.com).

Fault-tolerance: David Fura (dfura@jolt.boeing.com).

My interest is in the formal verification of fault-tolerant computers. I am currently at the dissertation proposal stage.

Real-time: Neil Viljoen (jnv@cl.cam.ac.uk).

Define a small language containing explicit timing constructs as defined by a deterministic scheduler. This environment should be seen as implementing some of the ideas from the world of process algebras, but with explicit real–time characteristics. Specify a scheduler in HOL and verify its safety and liveness properties. An evaluation of the constructs based on this approach will be done along with a final definition of the syntax and a formalisation of the semantics.

RTL: Jeff Joyce (joyce@cs.ubc.ca) (in collaboration with J. Rushby and associates at SRI Menlo Park).

Relationship between an RTL hardware model (expressed in HOL) and a conventional silicon compiler.

Self-timed systems: Jeff Joyce (joyce@cs.ubc.ca).

Beginning work on formal verification of Sutherland’s micropipelines using temporal logic notation embedded in HOL.

Instruction sets: Tej Arora (tej@charon.amdahl.com).

Our work demonstrates that microprocessor verification is enhanced by having the instruction set orthogonal; the original (RSRE) Viper Instruction set is very non-orthogonal. Thus, we re-specified the Viper instruction set as 20 orthogonal instructions. However, to assure that what we proved is the original Viper instruction set, we showed that an interpreter with these 20 instructions implies the 128 cases of the original Viper instruction set.

2 Systems

Very often it is more adequate to check correctness of hardware in more abstract terms, rather than in the circuit level. Also functionality is often spread over a combination of hardware and software, and it is important to reason about the combination as a whole. Verification at the systems levels fits in within a larger framework in which complex functionality is examined in several layers, and includes reasoning about the relevant software.

Distributed systems: Jim Alves-Foss (foss@iris.eecs.ucdavis.edu).

We use HOL as a verification tool to specify components of distributed computer systems. These components are modeled as event systems, where each component is specified according to the events of the component, input and output events, and the set of possible traces (histories of events) of the component.

Protocols: Rachel Cardell-Oliver (rco@sri.co.uk).

Protocols are modelled as predicates on histories (which are mappings from time to values representing input-output behaviour, state, etc.). I have shown how to construct generic specifications in this model which capture the behaviour common to a group of protocol algorithms such as sliding window protocols. I have also shown how real-time program code can be verified to satisfy such specifications by defining a program language semantics based on histories, and developing some HOL infrastructure for verification proofs about programs written in this language.

SAFEMOS: David Shepherd (des@inmos.co.uk), Mike Gordon (mjcg@cam.sri.com), Roger Hale (rwsh@cam.sri.com), John Herbert (jmjh@cam.sri.com), Jonathan Bowen (Jonathan.Bowen@prg.oxford.ac.uk), Juanito Camilleri (jac1@uk.ac.cam.cl) and others.

Design and build a small totally verified system by creating a verified application program running on a verified processor by means of a verified compiler. Develop a methodology for building verified hard real-time systems. Example driven with a programming language based on a subset of OCCAM, and a processor based on the Transputer. The project is similar in spirit to the CLINC stack (Austin, Texas) and Joyce’s work on Tamarack (Cambridge), but with greater emphasis on temporal aspects.

LOTUS: Steve Colwill (sjc@uk.co.bt.fmg).

Temporal semantics for a subset of Basic LOTOS. The idea is that the system description is provided in LOTOS, properties of interest are described in the TL (or other suitable notation embedded in a similar framework), and proofs that the LOTOS description has the properties described are carried out in the HOL framework. Paper submitted to FORTE’91.

System classes: Jim Alves-Foss (foss@iris.eecs.ucdavis.edu).

We have developed a set of generic system classes based on relationships of inputs to outputs (1-1, 1-many, many-1, many-many). We are beginning to show under which cases elements of these classes are restrictive, and how to instantiate elements to specific system components and automatically prove that they are restrictive (one restrictive proof takes 1 man-month, one instantiation proof takes 1 man-day – huge time savings!!).

Railway signalling: W J Cullyer and Wai Wong (esww@eagle.warwick.ac.uk or eswjc@eagle.warwick.ac.uk).

Scheduling: Glenn MacEwen (macewen@qucis.queensu.ca).

A run-time environment supporting deadline-driven scheduling and message-passing has been completed.

Generic Specifications: Jeff Joyce (joyce@cs.ubc.ca).

Development of a technique for writing generic specifications in higher-order logic (based on “representation variables”) that avoids unnecessary extensions to the HOL logic to support generic specification.

Protocol verification: Graham Birtwistle (graham@cpsc.ucalgary.ca).

We have explored a small protocol (alternating bit) in HOL learning much from Rachel Cardell-Oliver’s work. Development work will continue in 1991.

CASE tools: Jeff Joyce and students (joyce@cs.ubc.ca).

Linking ”next generation” CASE tools with HOL. We aim to develop an approach where highly comprehensible, executable specifications are created in a ”graphical specification language” using a tool such as i-Logix STATEMATE. These specifications will be suitable for all kinds of ”reactive systems” (hardware as well as software).

Z: Roger Jones (R.B.Jones@win0103.uucp) et. al., International Computers Limited.

Extensive use of Cambridge HOL system for reasoning about system specifications in Z, by partly automated translation of Z into HOL. Proof support for the full Z specification language based on the ICL implementation of HOL.

3 Calculii

Process algebras are abstractions about processes, allowing one to model issues such as concurrency, communication, and nondeterminism. Typical algebras are CSP and CCS. There has recently been a lot of interest in linking the descriptive power offered by the algebras to the formal reasoning capability of HOL.

CCS: Monica Nesi (mn@cl.cam.ac.uk).

CCS without value passing and a specific behavioural semantics, namely observational congruence, have been considered. The divergence of Knuth-Bendix completion of the axioms of the observational congruence for finite CCS has been considered. A rewriting strategy for deciding whether or not two finite CCS specifications are observational congruent (without attempting any completion) has been defined.

CCS: Juanito Camilleri (jac1@uk.ac.cam.cl).

Process Calculi — Preliminary work done on a definitional theory in HOL of CCS augmented with priority constructs (Ph.D thesis).

Process Algebras: Albert Camilleri (ac@hplb.hpl.hp.com).

Mechanizing process algebras.

CSP: Michael Benjamin (benjamin@src.bae.co.uk).

Implemented a version of the traces model of CSP as a conservative extension of HOL.

Pi-calculus: Tom Melham (tfm@cl.cam.ac.uk) and Mike Gordon (mjcg@cl.cam.ac.uk).

A definitional theory of the pi-calculus (Milner, Parrow, and Walker) in HOL. Status: fairly preliminary, but the bits that are done are finished to “production-quality”.

CSP: Kevin Blackburn (K.Blackburn@win0103.uucp), International Computers Limited.

Implementation of a fragment of CSP in HOL by defining the CSP operators and then deriving the proof rules (1987).

4 Software

The correctness of software is linked to the correctness of the compiler which implements the underlying semantics. Much of the work on program verification using HOL thus concentrates on the correctness of the compilation process. Other approaches concentrate of formally reasoning about certain aspects of programs, such as concurrency.

4.1 Compilers

Algebraic specifications: Jonathan Bowen (Jonathan.Bowen@prg.oxford.ac.uk).

At Oxford we have used HOL for some proofs of correctness of a compiling specification assuming a set of algebraic laws about the language. This makes use of inequations rather than equations. To make things easy for ourselves we have used equations and promised not to use them the wrong way in any proofs.

Denotational semantics: Jeff Joyce (joyce@cs.ubc.ca).

Formal verification of a compilation algorithm for a very simple imperative language targeted to very simple microprocessor (Tamarack-3); semantics is expressed denotationally; takes account of ‘finite limitations’ of hardware.

VISTA Translator: Paul Curzon (pc@cl.cam.ac.uk).

Define the semantics of VISTA in HOL. Define and verify a translator from VISTA to VIPER machine code written in the HOL logic. Define the syntax and a direct denotational semantics of both source and target language in HOL with the translator as a primitive recursive function.

Real-time systems: Roger Hale (rwsh@cam.sri.com).

Embedding real-time programming language semantics in HOL with a view to verifying properties of programs and the correctness of a simple compiler (as part of the SAFEMOS project). The semantics are based on interval temporal logic.

Compiler correctness: Graham Birtwistle (graham@cpsc.ucalgary.ca).

We have done some hand proofs and expect to start putting them into HOL in 1991.

4.2 Programming Methodology

Program refinement: Joakim von Wright (jwright@finabo.abo.fi).

Total correctness and program refinement. Aim is to formalize Dijkstra-style programming and specification languages and the notions of correctness and refinement in HOL. Furthermore, we prove the correctness of proof rules and program transformation rules.

Refinement calculator: Joakim von Wright (jwright@finabo.abo.fi).

The aim is to build an interactive environment for program development where all program transformations (refinements) are proved in HOL.

Formal semantics: Chris Brink (cbrink@ucthpx.uct.ac.za) and Ronnie Becker (rib@ucthpx.uct.ac.za).

We have just set up a Laboratory for Formal Aspects of Computer Science at the University of Cape Town. We are very interested in using HOL for formal semantics and verification.

Symbolic execution: Maris Ozols (maris@itd0.dsto.oz.au).

Program verification using symbolic execution; modelling concurrency; modelling finite state machines (for software specification, not hardware).

Security and concurrency: Tony Cant (cant@itd0.dsto.oz.au), Katherine Eastaughffe (kae@itd0.dsto.oz.au).

Reasoning about programs using denotational semantics; security policy modelling; modelling concurrency (CCS, CSP, and other techniques). Logics for reasoning about programs.

Control systems: Jonathan Jacky (jon@gaffer.rad.washington.edu).

Safety of medical devices that contain or use computers. Currently investigating formal approaches to specifying and developing software for the control system of a medical cyclotron that we use for neutron radiation therapy and isotope production.

Functional and Logic language: Shiu-Kai Chin (chin@cat.syr.edu).

We are using HOL to describe part of an implementation of a combined function/logic programming language. The implementation combines the Three Instruction Machine with the Warren Abstract Machine to support a language which looks like a combination of Haskell and Prolog.

Unwinding and authentication: David King (djk@win.icl.co.uk), International Computers Limited.

Work on applications in HOL include a formal proof of Goguen and Meseguer’s unwinding theorem. Also a prototype implementation of Burrows, Needham and Abadi’s authentication logic has been produced using the prototype ICL HOL.

5 Proof Development

Several attempts are being made to enhance the proof structure and methodology in HOL. This session covers attempts to both enrich the proof process by the use of more sophisticated techniques and to fit in the resulting proofs into a mathematical or verification environment.

Normality of proofs: Thomas Forster (tf@moa.pmms.cam.ac.uk).

Using HOL to examine known proofs. The particular question is whether or not some specific proof (the proof of the axiom of infinity in Quine’s set theory) is a normal proof. I would want to be able to build a proof interactively in the usual way, and then store it in such a way that i could call an ML program isnormal: proof -> bool that tests it. Probably not very difficult, though some of the applications software (isnormal for example) could be quite tricky.

Proof certification: Avra Cohn (avrac@cl.cam.ac.uk).

Understand the structure and parameterisation of large proofs; develop and test a technology for producing ‘proof deliverables’ (idea proposed by Newey, Hanna). Modify HOL to produce proof texts. Code a checker for them in a programming language supported by HOL. Better understanding of the relationship between proofs and tactics. Implementation of prototype tools to generate proof summaries from tactics.

Justifications: Sara Kalvala (kalvala@cs.ucdavis.edu).

Improving the interaction between design and verification. This is accomplished by using justifications presented by the designer. Justifications make explicit the reasons why the designer intuitively believes that a design satisfies its intent.

Inductive definitions: Tom Melham (tfm@cl.cam.ac.uk) and Juanito Camilleri (jac1@uk.ac.cam.cl).

A collection of tools (written by tfm) for deriving inductive definitions of predicates and for doing inductive proofs about them. This package almost ready for preliminary release. Tech reports on the tool (by tfm) and on some example applications (tfm and jac1) to appear.

P Omega: Kim Dam Petersen (kimdam@tfl.dk).

In this project the P-Omega model as described by Barendregt and Scott is defined as a definitional theory in the HOL system. The short term purpose of this project has been to be able to specify Remote Module Calls, which needs reflexive domains, in HOL. The long term purpose is to make a general package, like the type package of Tom Melham, which allows one to define any valid reflexive domain in HOL.

Equational inference Konrad Slind (slind@cpsc.ucalgary.ca):

Use of equational inference methods in HOL (Knuth-Bendix completion and AC rewriting); Knuth-Bendix completion has been implemented (as a derived rule of inference). I have solved the problem of how to do AC rewriting in HOL, but further investigation is required to see if it is actually useful.

5.1 Mathematics

Mathematical theories and models have also been realized in HOL, either to be used further in verification projects or to increase trust in the given theories.

Graph theory: W J Cullyer and Wai Wong (esww@eagle.warwick.ac.uk or eswjc@eagle.warwick.ac.uk).

We are working on a simple graph theory which will be the base of a formal model of railway networks.

Events: Jim Alves-Foss (foss@iris.eecs.ucdavis.edu).

We have developed a theory of event systems in HOL and a theory of sequences (i.e. lists with new elements added to the end of the sequence). The sequence theory has been specified and many theorems, operations, and such have been developed for it.

Temporal logic: Amit Jasuja (ajasuja@oracle.com).

Specification and verification of asynchronous circuits using temporal logic.

Events: Glenn MacEwen (macewen@qucis.queensu.ca).

Rather than a signal on a wire represented by a function of time, we use a stream of event occurrences, represented by a function that gives the time of the ith occurrence. This derives from Mok’s Real-time Logic (RTL). Event occurrence streams, unlike wires, are typed and there are some fundamental restrictions on how they can be combined in a specification. Another difference is that real-time components cannot be composed quite so freely as digital devices.

Lattice Theory: Joakim von Wright (jwright@finabo.abo.fi).

Abstract Lattice Theory in HOL. The aim is to prove lattice-theoretic results once and for all. These results can then be used in other theories.

Automata theory: Paul Loewenstein (melasv!paul@net.UU.uunet).

I have some theories covering some automata theory, although it is not the theory one typically finds in text books. They are potentially infinite. The theory is derived for labeled transition automata and labelled state automata. Because the state-space can be infinite, the automata can express non-safety properties. However, there is only a limited (but useful) class of non-safety properties that can be reasonably verified by simulation relations. It is currently being supplemented with a more powerful state-mapping technique which allows the two automata to make non-deterministic choices at different times. The difficult part (a proof of Koenig’s infinity lemma) has been done.

Set Theory: Roger Jones (R.B.Jones@win0103.uucp), International Computers Limited.

Classical set theory in HOL introduced by adding a new type SET and axioms corresponding to the axioms of Zermelo- Fraenkel set theory (except that separation turns out stronger when stated naturally into HOL). Several theories developed over the top of this for purpose of research into logical foundation systems which could not have been achieved by conservative extension of HOL. Formalisation of parts of category theory in HOL for self educational purposes. Up to the definition of adjunction. No proofs.

UNITY: Flemming Andersen (fa@tfl.dk).

Use higher order logic to formalise the UNITY theory as it is described in the book by Chandy and Misra, Parallel Programming: a Foundation. Get a mechanized proof system for UNITY using the HOL system. This work is about to be finished.

Data structures: Konrad Slind (slind@cpsc.ucalgary.ca).

Investigation of data structures and algorithms for logic implementation; currently investigating the use of deBruijn terms.

5.2 The HOL System

Several enhancements to the HOL system are being developed, ranging from completely new implementations to more theorem-proving tools. There also is an emphasis in making HOL easier to learn, through courses offered by experts.

HOL90: Konrad Slind (slind@cpsc.ucalgary.ca) and Graham Birtwistle (graham@cpsc.ucalgary.ca).

New implementation of HOL in SML. We hope to release it next july after further restructuring with the help of AT&T and some help from Cambridge to ensure that it is fully compatible with the then current release of HOL88.

ICL HOL: Roger Jones (R.B.Jones@win0103.uucp) et. al., International Computers Limited.

Industrial quality implementation of HOL using standard ML as metalanguage. Prototype in use internally since May 1990. Basic product quality implementation now in place (August 1991).

Tactics: Katherine Eastaughffe (kae@itd0.dsto.oz.au).

Development of quite a few tactics for manipulating assumptions more finely (using their numbering) and in rewriting and applying conversions to selected subterms of the goal.

Interface tools: Sara Kalvala (kalvala@iris.ucdavis.edu).

Improve the HOL proof environment through new facilities for goal management and documentation browsing, as well as an X-based user interface.

Front-end: Michael Benjamin (benjamin@src.bae.co.uk).

I’m using a graphical interface called SPIRITS to implement a ‘user friendly’ front end. This includes an interface to make working in HOL slightly easier – e.g.: it displays a proof tree during goal directed proof so you can see the structure of the proof.

Textbook: Graham Birtwistle (graham@cpsc.ucalgary.ca).

A text on HOL (started in 1987) is slowly getting into shape and could be released as a draft in July 1991.

HOL Course: Jeff Joyce (joyce@cs.ubc.ca), Rachel Cardell-Oliver (rco@sri.co.uk) and John Herbert (jmjh@sri.co.uk).

5-day course on the HOL system; offered in June 1990 and April 1991.

HOL Course: Tom Melham (tfm@cl.cam.ac.uk).

I have developed a 5-day intensive training course on the HOL system. This was first taught at Calgary in 1986 and has been taught at several other sites since then. I am always open to proposals to run the course again, either in industry or in academia.

Specification: Rob Arthan (rda@win.icl.co.uk), International Computers Limited:

Full formal specification of HOL in (ICL concrete representation of) HOL covers language, semantics, proof rules, critical properties of proof development system (produced as part of ICL HOL development).