Ebook: Proof Technology and Computation

This volume contains elaborations of the lectures given at the Marktoberdorf Summer School 2003 on “Proof Technology and Computation”, the 24th of a series of Advanced Study Institute sponsored by the NATO Scientific and Environmental Affairs Division.

Nowadays, “Proof technology” will become an established field in software engineering. It generally aims at integrating proof processing into industrial design and verifications tools. The origins of this technology lie in the systematic understanding of a fully-fledged, precise notion of proof by mathematics and logics. Using this profound understanding computer scientists are able to implement proofs, to check and create them automatically and to connect the concepts of proof and programs in a deep way. Via this, connection proofs are used to support the development of reliable software systems. Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The Summer School 2003 at Marktoberdorf gave a detailed and profound overview on actual researching results and its industrial application around this proof technology.

Robert Constable lectured on the benefits and technical challenges of sharing formal mathematics among interactive theorem provers. The goal of Gilles Dowek was to present classical results on proof normalization for various axiomatic theories using a newly proposed formulation of predicate logic, called deduction modulo, where a theory is defined by a set of axioms and rewrite rules. Orna Grumberg presented an abstraction-refinement framework of temporal logic model checking, which has then been extended to deal with 3-valued abstraction, game-based model checking and full CTL.

John Harrison demonstrated, that formal verification is an increasingly important topic in industrial hardware design. He gave a broad overview of the main techniques currently being used for industrial-scale hardware verification with special attention to the construction of interactive theorem provers using the “LCF” approach. Highlights of several important topics concerning relations between the theory of computability and computational complexity on the one hand, and programming languages on the other were presented by Neil D. Jones. Tobias Nipkow lectured on readable machine-checked proofs and semantics, based on Isabelle/HOL and Isar, as well as the application of this theorem proving framework to the specification and analysis of operational semantics for Jinja, a Java-like language.

The lecture series from Michael Rathjen were concerned with an intuitionistic and predicative theory of types developed by Martin-Löf and a constructive version of Zermelo-Fraenkel set theory inaugurated by Myhill and further developed by Aczel. Helmut Schwichtenberg has shown the important point in exact real numbers, as opposed to floating point numbers and to develop the basics of real analysis in such a way that from a proof of an existence formula one can extract a program. Pawel Urzyczyn lectured on predicates as types. The covered issues were related to the Curry-Howard Isomorphism for predicate logic, including first-order intuitionistic logic and arithmetic.

Moshe Y. Vardi's course provided an introduction to the theory of automata on infinite objects and demonstrates its applications to design specification, verification, and synthesis. The automata-theoretic approach to design verification uses the theory of automata as a unifying paradigm. Stanley S. Wainer lectured fundamental ideas from mathematical logic and proof theory, connecting the computational complexity of recursions with the logical complexity of their termination-proofs.

The Summer School has been two weeks of learning, discussing and developing new ideas, and a gainful event, both from the professional and from the social aspect. Again, the Summer School benefited a lot from the experienced scientific staff from Munich and the local Marktoberdorf crew. Our sincere thanks go to all of them.

The Editors

This paper presents two frameworks for abstraction-refinement in model checking. The first one handles ACTL specification. The abstraction is conservative for ACTL verification, but not for falsification. Spurious counterexamples in the abstract model are used to guide a refinement that eliminates these counterexamples.

The other framework handles full CTL. On abstract models, CTL formulas are interpreted with respect to the 3-valued semantics and can be evaluated to either true, false, or the indefinite value ⊥. The abstraction is conservative for CTL verification as well as falsification. Only if a formula is evaluated to ⊥ in the abstract model, its value in the concrete model is unknown and refinement is needed. However, now the goal of the refinement is to eliminate indefinite results and to turn them into either definite true or definite false.

These lectures are intended to give a broad overview of the most important formal verification techniques that are currently used in the hardware industry. They are somewhat biased towards applications of deductive theorem proving (since that is my special area of interest) and away from temporal logic model checking (since there are other lectures on that topic). The arrangement of material is roughly in order of logical complexity, starting with methods for propositional logic and leading up to general theorem proving, then finishing with an extended case study on the verification of a floating-point square root algorithm used by Intel.

1. Propositional logic

2. Symbolic simulation

3. Model checking

4. General theorem proving

5. HOL Light

6. Case study of floating-point verification

My original plan was to lecture on items 1–4 and 6 in the above list. However, since Orna Grumberg presented temporal logic model checking in much more detail, I dropped the lecture on this topic, section 3 here, replacing it by a detailed discussion of HOL Light, which forms section 5 here. The following notes include all this material.

The treatment of the various topics is quite superficial, with the aim being overall perspective rather than in-depth understanding. The last lecture is somewhat more detailed and should give a good feel for the realities of formal verification in this field.

These notes draw on my forthcoming book on automated theorem proving, and simple-minded example code (written in Objective Caml) illustrating many of the techniques described can be found on my Web page:

http://www.cl.cam.ac.uk/users/jrh/atp/index.html

Jinja is a Java-like programming language with a formal semantics designed to exhibit core features of Java. It is a compromise between realism of the language and tractability and clarity of the formal semantics. A big and a small step operational semantics are defined and shown equivalent. A type system and a definite initialization analysis are defined and type safety of the small step semantics is shown. The whole development has been carried out in the theorem prover Isabelle/HOL.

The main objective of this paper is to show that a certain formulae-as-classes interpretation based on generalized set recursive functions provides a self-validating semantics for Constructive Zermelo-Fraenkel Set theory, CZF. It is argued that this interpretation plays a similar role for CZF as the constructible hierarchy for classical set theory, in that it can be employed to show that CZF is expandable by several forms of the axiom of choice without adding more consistency strength.

This lecture concerns issues related to the Curry-Howard Isomorphism for predicate logic, mostly first-order logic and first-order arithmetic. We discuss the relationship between predicate logics and the corresponding propositional logics, obtained via dependency-erasing operators. Rather than showing new results, the lecture aims at explaining basic ideas and clarifying some issues which belong to the very fundamentals of the proof technology. In particular, we consider lambda calculi corresponding to predicate logic and arithmetic, an we point out the relation between strong normalization and proof extraction. These lecture notes are based in part on a joint work with Morten Heine Sørensen [23].

The automata-theoretic approach to linear temporal logic uses the theory of automata as a unifying paradigm for program specification, verification, and synthesis. Both programs and specifications are in essence descriptions of computations. These computations can be viewed as words over some alphabet. Thus, programs and specifications can be viewed as descriptions of languages over some alphabet. The automata-theoretic perspective considers the relationships between programs and their specifications as relationships between languages. By translating programs and specifications to automata, questions about programs and their specifications can be reduced to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of programs with respect to their specifications can be reduced to questions such as nonemptiness and containment of automata.

Unlike classical automata theory, which focused on automata on finite words, the applications to program specification, verification, and synthesis, use automata on infinite words, since the computations in which we are interested are typically infinite. This paper provides an introduction to the theory of automata on infinite words and demonstrates its applications to program specification, verification, and synthesis.

These lecture notes aim to provide a reasonably detailed introduction to some of the mathematics underpinning the theory of recursion and its interrelationships with proof theory. General results about hierarchies of “fast” and “slow” growing bounding functions are developed, in order: (i) to give a direct link between the computational complexity of recursions and the logical complexity of their termination proofs, and (ii) to show how the general notions of recursion and proof may be restricted so as to characterize computationally “realistic” complexity classes.