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.
Lindsay Groves & Bill Flinn
Provides a short overview of formal methods, with emphasis on formal specifications. Basically an introductory paper.
Jonathan P. Bowen & Michael G. Hinchey
Discusses common misconceptions about formal methods. Sort of a followup to Hall's original "7 Myths" article.
Edsger Dijkstra
Philosophical and social reflections on the reasons why program correctness is so underappreciated.
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.
J.R. JEFFERSON WADKINS
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.
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.
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.
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.
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.
CHRIS HANKIN, HANNE RIIS NIELSON, JENS PALSBERG, ET AL
Covers various areas in programming language research and areas or future interest. Includes sections on formalism and semantics.
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.
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.
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/Intl_FM_Survey_vol2_1997.ps
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.
Roderick Chapman
Discusses 4 industrial projects that used SPARK - 3 successes and one less so.
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.
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.
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.
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.
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.
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.
Roderick Chapman
Discusses the CC and ITSEC requirements and how SPARK meets them. Also discusses the MULTIOS CA smart-card system.
Peter Amey
Another article describing SPARK. Discusses how static analysis improves design by catching problems early. Includes short case study.
Peter Amey
Article from Praxis describing SPARK and how correctness by construction can reduce costs. Gives example of SPARK project for Lockheed.
C. A. R. Hoare
Introduction of Hoare logics and the {P}S{Q} notation.
HANS-JUERGEN BOEHM
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."
David Gries
Defines proof rules for the general case of multiple assignment as well as for procedure calls with in/out parameters.
SHAULA YEMINI & DANIEL M. BERRY
Gives an axiomatic replacement-rule definition for exceptions. Only requires two new proof rules in the general case. Includes example program.
Edsger W.Dijkstra
Introduces Dijkstra's calculus for guarded commands and how to derive programs using them.
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.
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.
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.
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.
Alain Deutsch
Short "tutorial" on alias analysis related to pointers and dynamic allocation.
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.
ARTHUR J. NEVINS
Describes a system (presumably) for automatic theorem-provers that combines resolution with natural deduction. Apparently it compares well with existing theorem-provers.
JAMES R.SLAGLE
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.
Roderick Chapman
Short paper regarding Abstract Interpretation technology for static analysis of code. Tries to dispell AI myths when compared to SPARK.
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.
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.
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.
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.
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)
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++.
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.
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.
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.
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.
JOHN C. CHERNIAVSKY & SAMUEL N. KAMIN
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.
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.
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
Ana Cavalcanti and David Naumann
Lecture slides from a presentation on the semantics of an object-oriented language, presumably ROOL.
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.
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.
MANFRED BROY & GREG NELSON
Appears to be a revision/summary/rehash/republication of Nelson & Broy's 1989 paper Can Fair Choice Be Added to Dijkstra's Calculus?
EDMUND MELSON CLARKE JR.
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.
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.
EDMUND M. CLARKE JR., STEVEN M. GERMAN, & JOSEPH Y. HALPERN
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,
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.
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.
James Barnes, Brian Dobbing, & Rod Chapman
Discusses SPARK and how some object-orientation has been incorporated into it.
Peter Amey & Roderick Chapman
Discusses SPARK and the approach it takes to demonstrating the absence of run-time exceptions.
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.
Peter Baumann
Mailing list posting calling for and citing formal semantics for real-world programming languages.
Jason Gorman
An editorial discussing eXtreme Programming with relation to formal methods.
Tony Hoare's Turing Award lecture, in which he lambasts Ada and reflects on his development work.