Formal Methods

Peter Peter A. Geer

1 Methodology and Practical Applications

1.1 Methodology Discussions

1.1.1 10 Commandments of Formal Methods

Jonathan P. Bowen & Michael G. Hinchey

A set of informal guidelines for use with formal methods projects. Addesses some of the practical, non-mathematical concerns.

Full article (PDF)

1.1.2 The Case for Formal Methods in Software Development

Lindsay Groves & Bill Flinn

Provides a short overview of formal methods, with emphasis on formal specifications. Basically an introductory paper.

Full text (PDF)

1.1.3 Seven More Myths of Formal Methods: Dispelling Industrial Prejudices

Jonathan P. Bowen & Michael G. Hinchey

Discusses common misconceptions about formal methods. Sort of a followup to Hall's original "7 Myths" article.

Full text (PDF)

Notes (plain text)

1.1.4 Correctness Concerns And, Among Other Things, Why They Are Resented

Edsger Dijkstra

Philosophical and social reflections on the reasons why program correctness is so underappreciated.

Ful text (PDF)

1.1.5 Formal Methods When Money is Tight

Marsha Chechik & Andre Wong

Briefly discusses how FM can be used in commercial projects where quality is not a chief concern. Discusses how FM can keep costs down, with emphasis on telecom.

Full text (PDF)



Describes three ways to derive programs with "built-in correctness" in the spirit of Dijkstra, Hoare, and Gries, but without using the notation of formal axiomatic semantics. The reasoning is mathematical, but not formally so.

Full text (PDF)

1.1.7 Static Verification and Extreme Programming

Peter Amey & Roderick Chapman

Discusses how some of the practices used for high integrity systems are similar to XP. Includes discussion of SPARK and how static verification can be used in refactoring.

Full text (PDF)

1.2 JAX: Systematic Java Testing with JUnit and Axioms

Describes a method for generating JUnit test classes. Based on the algabraic specification for abstract data types. These algabraic specifications of classes are used as axioms.

Full text (Word doc)

1.3 Surveys and Broad Overviews

1.3.1 Formal Methods: State of the Art and Future Directions

Edmund M. Clarke & Jeannette M. Wing

Provides a survey of formal methods being used in hardware and software development. Also discusses advances in methods and tools.

Full text (PDF)

1.3.2 Formal Methods for the Analysis of Authentication Protocols

A. D. Rubin & P. Honeyman

An analysis of how formal methods are applied to cryptographic protocols. Breaks the methods into four categories:

Type I - uses generic FM tools (not particular to cryptography).

Type II - analyze using expert system.

Type III - uses logics designed to dealing with questions of knowledge and belief.

Type IV - uses algebraic term rewriting.

Full text (PDF)

1.3.3 Strategic Directions in Research on Programming Languages


Covers various areas in programming language research and areas or future interest. Includes sections on formalism and semantics.

Full text (PDF)

1.3.4 Formal Methods and Certification of Critical Systems

John Rushby

An extensive guide to the various aspects of formal methods targeted at engineers. This is s supplement to the FAA's Digital Systems Validation Handbook and is primarily aimed at on-board computers for aircraft.

Full text (PostScript)

1.4 Case Studies

1.4.1 An Internationsl Survey of Industrial Applications of Formal Methods, Volume 1: Purpose, Approach, Analysis, and Conclusions

Dain Craigen, Susan Gerhart, & Ted Ralston

First volume of the study that covered 12 major formal methods projects. This volume describes the cases, formal methods used, and approach to the study.

Full text (PostScript)

  1. An Internationsl Survey of Industrial Applications of Formal Methods, Volume 2: Case Studies

    Dain Craigen, Susan Gerhart, & Ted Ralston

    Volme 2 of the 12 case studies paper. This contains the actual case studies, including descriptions, data summaries, evaluation, and describes some FM-related R&D issues.

    /home/pageer/misc/Thesis/Research Papers/

1.4.2 An Invoicing Case Study in Z

Jonathan P. Bowen

Describes an answer to a challenge to examine the questions raised by specifying things in a formal manner to the ones raised by English specifications. The system is an invoicing system with a Z specification.

Full text (PDF)

1.4.3 Industrial Experience with SPARK

Roderick Chapman

Discusses 4 industrial projects that used SPARK - 3 successes and one less so.

1.4.4 Is Proof More Cost-Effective Than Testing?

Steve King, Jonathan Hammond, Rod Chapman, & Andy Pryor

Discusses SHOLIS (Ship Helicopter Operating Limits Information System), a system developed under UK defense standards requiring formal methods. Used SPARK and Z and discusses the proofs involved and the efficacy of them.

Full text (PDF)

1.4.5 Correctness by Construction: Developing a Commercial Secure System

Anthony Hall & Roderick Chapman

Article describing commercial Smart Card security systems designed by Praxis. Includes use of SPARK and Z, as well as off-the-shelf Windows NT and other components.

Full text (PDF)


Kate Finney & Norman Fenton

Examines IBM's use of Z in the development of CICS. This was largely hailed as a success for formal methods, but the authors are unconvinced by the data that formal methods can be widely applied to commercial projects.

Full text (PDF)

1.4.7 An Analysis of Two Formal Methods: VDM & Z

Thomas McGibbon

Compares and contrasts Z and VDM, to each other and to other FM approaches, as well as Cleanroom and other process improvements. Includes sections on tools support and return on investment.

Full text (PDF)

1.4.8 Why Are Formal Methods Not Used More Widely?

John C. Knight, Colleen L. DeJong, Matthew S. Gibble, & Luís G. Nakano

Used case studies of "significant applications" to determine why FM are not more widely used. Present an evaluation framework and discuss some of the practical shortcoming of FM, including tools.

Full text (PDF)

Notes (plain text)

1.4.9 Lightweight Formal Methods Applied to a Radiation Therapy Machine Component

Greg Dennis, Robert Seater, Derek Rayside & Daniel Jackson

Applied FM to the beam scheduling specification for a radiation therapy device and discovered bugs due to concurrency issues, i.e. two people can start the machine at once. Uses Alloy modeling language.

Full text (PDF)

Notes (plain text)

1.4.10 SPARK

  1. SPARK - A state-of-the-practice approach to the Common Criteria implementation requirements

    Roderick Chapman

    Discusses the CC and ITSEC requirements and how SPARK meets them. Also discusses the MULTIOS CA smart-card system.

    Full text (PDF)

  2. Closing the Loop: The Influence of Code Analysis on Design

    Peter Amey

    Another article describing SPARK. Discusses how static analysis improves design by catching problems early. Includes short case study.

    Full text (PDF)

  3. Correctness by Construction: Better Can Also Be Cheaper

    Peter Amey

    Article from Praxis describing SPARK and how correctness by construction can reduce costs. Gives example of SPARK project for Lockheed.

    Full text (PDF)

2 Academic and Theoretical Considerations

2.1 Semantics Theory

2.1.1 An Axiomatic Basis for Computer Programming

C. A. R. Hoare

Introduction of Hoare logics and the {P}S{Q} notation.

Full text (PDF)

2.1.2 Side Effects and Aliasing Can Have Simple Axiomatic Descriptions


Gives axiomatic definition of Algol-68 type imperative languages that don't distinguish between statements and expressions. Uses the expression values rather than pre- and post-conditions as underlying primitive. This makes side effects and aliasing "easily axiomatizable."

Full text (PDF)

2.1.3 Assignment and Procedure Call Proof Rules

David Gries

Defines proof rules for the general case of multiple assignment as well as for procedure calls with in/out parameters.

Full text (PDF)

2.1.4 An Axiomatic Treatment of Exception Handling in an Expression-Oriented Language


Gives an axiomatic replacement-rule definition for exceptions. Only requires two new proof rules in the general case. Includes example program.

Full text (PDF)


Edsger W.Dijkstra

Introduces Dijkstra's calculus for guarded commands and how to derive programs using them.

Alternate full text (PDF)

Full text (PDF)

2.1.6 A Critique of the Foundations of Hoare Style Programming Logics

Michael J. O'Donnell

Discusses some rules of Hoare logic that are not "inferentially sound". This is opposed to "theorem soundness," which is what you would get in an incomplete system, i.e. the hypotheses plus inference rules cannot prove some true statements.

The author seems to be saying that the logic is geared towards partial correctness, but that this is unacceptable. In addition, the use of goto statements viscerates Hoare logic.

Full text (PDF)

2.1.7 Hoare Logics for Recursive Procedures and Unbounded Nondeterminism

Tobias Nipkow

Gives sound and complete Hoare logic for recursive, parameterless procedures that can include unbounded nondeterminism. Apparently this had not been done before. Proofs checked with Isabelle/HOL.

Full text (PDF)

2.1.8 A Categorical Model for Higher Order Imperative Programming

David A. Naumann

Some kind of semantic model involving pre-ordered sets and higher order things and spans, whatever they are. In short, I have no idea what this is about.

Full text (PostScript)

2.1.9 Procedures in the Refinement Calculus: A New Approach?

Lindsay Groves

Discusses the use of procedures in the refinement calculus and some of the problems they cause for development not done in a strictly top-down fashion. Presents an alternative where code is packaged into procedures independent of algorithmic design decisions.

Full text (PDF)

2.1.10 Semantic Models and Abstract Interpretation Techniques for Inductive Data Structures and Pointers

Alain Deutsch

Short "tutorial" on alias analysis related to pointers and dynamic allocation.

Full text (PDF)

2.1.11 Algebraic Approaches to Nondeterminism: An Overview

A broad overview of the issues involved in working with nondeterminism. Includes algebras for dealing withthe semantics of nondeterminism. These appear to be based in large part on set theory and include a disturbing number of references to power sets.

Full text (PDF)

2.2 Theorem Proving

2.2.1 Human Oriented Logic for Automatic Theorem-Proving


Describes a system (presumably) for automatic theorem-provers that combines resolution with natural deduction. Apparently it compares well with existing theorem-provers.

Full text (PDF)

2.2.2 Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets


Discusses replacing various axioms of certain systems to take advantage of the structure of special theories, in particular equality, partial ordering, and set theory. The idea is that by "building in" these theories, refutation completeness is maintained but the system becomes more efficient, in that a computer should be able to resolve them faster and certain problems are avaoided.

Full text (PDF)

2.3 SPARK and Abstract Interpretation—A White Paper

Roderick Chapman

Short paper regarding Abstract Interpretation technology for static analysis of code. Tries to dispell AI myths when compared to SPARK.

Full text (PDF)

2.4 Verifications

2.4.1 Axiomatic Semantics Verification of a Secure Web Server

Paul E. Black

Doctoral thesis in which thttpd (Trivial HTTPD) is formally verified using an axiomatic semantics. Includes groundwork of formalizing the semantics of C.

Full text (PDF)

Notes (plain text)

2.4.2 Formal Verification of a Java Compiler in Isabelle

Martin Strecker

Describes a formal proof of correctness of a source-to-bytecode compiler for non-trivial subset of Java. Uses the proof environment "Isabelle" and is based on previous formalization work. Emphasises the effects of decisions about the formalizations on the correctness proof.

Full text (PDF)

Notes (plain text)

2.4.3 Proving Pointer Programs in Higher-Order Logic

Farhad Mehta and Tobias Nipkow

Describes a formal reasoning method for pointers. The programming language is "embedded in higher-order logic" and its Hoare logic is derived. Includes a case study with a proof using Isabelle/HOL.

Full text (PDF)

2.4.4 A Brief Account: Implementation and Applications of a PASCAL Program Verifier

David C. Luckham

An overview of the Stanford Pascal Verifier. Includes a technical overview as well as discussion of the assertion and rule languages, as well as an example program.

Full text (PDF)

2.4.5 A tool for symbolic program verification and abstraction

Susanne Graf & Claire Loiseaux

Describes a verification tool that involves verifying abstract programs and showing an equivaoence relation between those and concrete programs. This allows for a framework for automatic verification. Apparently the programs are internally represented as sets of Binary Decision Diagrams

Full text (compressed PostScript)

2.5 Student Case Studies and Exercises

2.5.1 The Undergraduate Capstone Software Design Experience

Jean R. S. Blair, Eugene K. Ressler, & Thomas D. Wagner

Describes large object-oriented compiler project for undergrads. Uses Ada95 and compares with Pascal and C++.

Full text (PDF)

2.5.2 Formal Methods Application: An Empirical Tale of Software Development

Ann E. Kelley Sobel

Covers a project in which elevator control systems were designed by two groups of undergrads, one using formal specifications (first-order logic), the other using no formal analysis. The formal methods group is seen to provide the better solution.

Full text (PDF)

2.5.3 An Exercise in Denotational Semantics

Describes method used for graduate-level FM course, whereby the denotational semantics of a programming language is taught by having students translate semantic equations directly into Prolog. The result is to build an interpreter, which helps make the semantics more concrete.

Full text (PDF)

2.6 Language Descriptions

2.6.1 A Weakest Precondition Semantics for Refinement of Object-Oriented Programs

Ana Cavalcanti & David A. Naumann

Describes a semantics for object-oriented languages that includes notions of visibility, dynamic binding, and recursion. Uses a weakest-precondition type semantics.

The target language is ROOL (Refinement Object-Oriented Language), a Java-like language the authors use for research.

Full text (PDF)

  1. A Weakest Precondition Semantics for an Object-Oriented Language of Refinement

    Ana Cavalcanti & David A. Naumann

    Describes the wp() semantics of ROOL, which contains recursion, visibility control, and dynamic binding. Deals with recursion by introducing a notion of refinement, for which constructs are monotonic.

    Full text (PostScript)

2.6.2 A Complete and Consistent Hoare Axiomatics for a Simple Programming Language


Introduces a language with a complete Hoare axiom system. Proves completeness of the system and introduces notion of complexity of Hoare systems based on proof length.

Full text (PDF)

2.6.3 How to define a language using PROLOG

Chris D. S. Moss

A "practical guide" to writing a programming language definition using Metamorphosis Grammar (M-Grammer) and Prolog. Includes context-sensitive syntax and denotational, relational, or axiomatic semantics. Could be extended to make Prolog-based compiler generator or automated program prover.

Full text (PDF)

2.6.4 On a Specification-oriented Model for Object-orientation

Ana Cavalcanti & David A. Naumann

Another paper describing ROOL. Apparently, ROOL uses constructs from Morgan's refinement calculus and includes specification statements as actual program statements. Or something.

ROOL's semantics is a set-based predicate transformer semantics, as opposed to the formula-based

Full text (PostScript)

  1. On a Specification-oriented Model for Object-orientation

    Ana Cavalcanti and David Naumann

    Lecture slides from a presentation on the semantics of an object-oriented language, presumably ROOL.

    Slides (PDF)

2.6.5 Predicate Transformer Semantics of a Higher Order Imperative Language with Record Subtyping

David A. Naumann

Gives a total-correctness semantics for a Higher Order language that includes record types, variable of type "procedure," and (subject to restrictions) global variables. Uses this to validate some simple proof rules. Language is similar to Oberion.

Full text (PostScript)

2.6.6 Can Fair Choice Be Added to Dijkstra's Calculus?

Manfred Broy & Greg Nelson

Discusses the implications of adding a nondeterministic choice operator to Dijkstra's guarded command language. Nelson previously extended the language to include recursion, defining a recursive program by a least fixpoint.

The "fairness" comes in the fact that the choice can be made by scheduling two tasks in parallel and picking the one to finish first. Again, the meaning of the choice is defined in terms of fixpoints.

Full text (PDF)

Alternate text (PostScript)

  1. Adding Fair Choice to Dijkstra’s Calculus


    Appears to be a revision/summary/rehash/republication of Nelson & Broy's 1989 paper Can Fair Choice Be Added to Dijkstra's Calculus?

    Full text (PDF)

2.6.7 Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems


Describes particular combinations of language constructs which make it impossible to get a sound and complete Hoare axiomatics. Apparently this applies even with the restrictions used by Cook to demonstrate a limited form of completeness.

Full text (PDF)


Joseph Y. Halpern

Discusses Clarke's demonstration that there is no complete axiom system for languages with certain properties. This shows that a complete axiomatization is possible if a more powerful assertion language than first-order logic.

Full text (PDF)

2.6.9 Effective Axiomatizations of Hoare Logics


Describes a class of programming languages (P) and "expressive interpretations" (I) for which there are sound and "relatively complete" Hoare logics for both partial correctness and termination assertions. Also draws link between decidability of theorems in I and the halting problem for P,

Full text (PDF)

2.6.10 Ecstatic: An object-oriented programming language with an axiomatic semantics

K. Rustan M. Leino

Describes an object-oriented language with an axiomatic semantics. Uses Dijkstra's weakest liberal precondition and features the ability to handle aliases.

Alternate copy (PDF)

Full text (PDF)

2.6.11 SPARK

  1. A Language for Systems Not Just Software

    Peter Amey

    Discusses how SPARK's annotations have developed into a way to integrate specification and implementation. That is, how the system specification is now parallel to the implementation details.

    Full text (PDF)

  2. On the Principled Design of Object Oriented Programming Languages for High Integrity Systems

    James Barnes, Brian Dobbing, & Rod Chapman

    Discusses SPARK and how some object-orientation has been incorporated into it.

    Full text (PDF)

  3. Industrial Strength Exception Freedom

    Peter Amey & Roderick Chapman

    Discusses SPARK and the approach it takes to demonstrating the absence of run-time exceptions.

    Full text (PDF)

  4. SPARK 95 - The SPADE Ada 95 Kernel (including RavenSPARK)

    Rod Chapman & Peter Amey

    Reference manual for the Ada 95 version of SPARK. Intended to be read along with the ARM95, not as a tutorial.

    Full text (PDF)

3 Miscellaneous Items

3.1 formal semantics of real-world programming languages lists

Peter Baumann

Mailing list posting calling for and citing formal semantics for real-world programming languages.

Full text (plain text)

3.2 Is XP Really Software Engineering?

Jason Gorman

An editorial discussing eXtreme Programming with relation to formal methods.

Full text (HTML)

3.3 The Emperor's Old Clothes

Tony Hoare's Turing Award lecture, in which he lambasts Ada and reflects on his development work.

Full text (PDF)