From 27a6c3636e8a29e74cd7f58e4e93c30a0e05334e Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 1 Apr 2018 19:44:48 0400
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Benton, Nick}
\index{Zarfaty, Uri}
\begin{chunk}{axiom.bib}
@inproceedings{Bent07,
author = "Benton, Nick and Zarfaty, Uri",
title = {{Formalizing and Verifying Semantic Type Soundness of a
Simple Compiler}},
booktitle = "Principles and Practice of Declarative Programming",
publisher = "ACM",
pages = "112",
year = "2007",
abstract =
"We describe a semantic type soundness result, formalized in the Coq
proof assistant, for a compiler from a simple imperative language with
heapallocated data into an idealized assembly language. Types in the
highlevel language are interpreted as binary relations, built using
both secondorder quantification and a form of separation structure,
over stores and code pointers in the lowlevel machine.",
paper = "Bent07.pdf",
keywords = "printed"
}
\end{chunk}
\index{Chlipala, Adam J.}
\begin{chunk}{axiom.bib}
@article{Chli07,
author = "Chlipala, Adam J.",
title = {{A Certified TypePreserving Compiler from the Lambda Calculus
to Assembly Language}},
journal = "ACM SIGPLAN PLDI'07",
volume = "42",
number = "6",
year = "2007",
pages = "5465",
abstract =
"We present a certified compiler from the simplytyped lambda calculus
to assembly language. The compiler is certified in the sense that it
comes with a machinechecked proof of semantics preservation,
performed with the Coq proof assistant. The compiler and the terms of
its several intermediate languages are given dependent types that
guarantee that only welltyped programs are representable. Thus, type
preservation for each compiler pass follows without any significant
"proofs" of the usual kind. Semantics preservation is proved based on
denotational semantics assigned to the intermediate languages. We
demonstrate how working with a typepreserving compiler enables
typedirected proof search to discharge large parts of our proof
obligations automatically.",
paper = "Chli07.pdf"
}
\end{chunk}
\index{Crary, Karl}
\index{Sarkar, Susmit}
\begin{chunk}{axiom.bib}
@misc{Crar08,
author = "Crary, Karl and Sarkar, Susmit",
title = {{Foundational Certified Code in a Metalogical Framework}},
link = "\url{http://repository.cmu.edu/compsci/470/}",
year = "2008",
abstract =
"Foundational certified code systems seek to prove untrusted programs
to be safe relative to safety policies given in terms of actual
machine architectures, thereby improving the systems' flexibility and
extensibility. Using the Twelf metalogical framework, we have
constructed a safety policy for the IA32 architecture with a trusted
runtime library. The safety policy is based on a formalized
operational semantics. We have also developed a complete, foundational
proof that a fully expressive typed assembly language satisfies that
safety policy",
paper = "Crar08.pdf"
}
\end{chunk}
\index{Fox, Anthony}
\begin{chunk}{axiom.bib}
@article{Foxx03,
author = "Fox, Anthony",
title = {{Formal Specification and Verification of ARM6}}
journal = "LNCS",
volume = "2758",
pages = "2540",
year = "2003",
abstract =
"This paper gives an overview of progress made on the formal
specification and verification of the ARM6 microarchitecture using
the HOL proof system. The ARM6 is a commercial processor design preva
lent in mobile and embedded systems – it features a 3stage pipeline
with a multicycle execute stage, six operating modes and a rich
32bit RISC instruction set. This paper describes some of the
difficulties encountered when working with a full blown instruction
set architecture that has not been designed with verification in mind.",
paper = "Foxx03.pdf"
}
\end{chunk}
\index{Guttman, Joshua D.}
\index{Ramsdell, John D.}
\index{Wand, Mitchell}
\begin{chunk}{axiom.bib}
@article{Gutt95,
author = "Guttman, Joshua D. and Ramsdell, John D. and Wand, Mitchell",
title = {{VLISP: A Verified Implementation of Scheme}},
journal = "Lisp and Symbolic Computation",
volume = "8",
pages = "532",
year = "1995",
abstract =
"The VL!SP project showed how to produce a comprehensively verified
implementation for a programming language, namely Scheme. This paper
introduces two more detailed studies on VLISP [13, 21). It summarizes
the basic techniques that were used repeatedly throughout the effort.
It presents scientific conclusions about the applicability of the
these techniques as well as engineering conclusions about the crucial
choices that allowed the verification to succeed.",
paper = "Gutt95.pdf"
}
\end{chunk}
\index{Leroy, Xavier}
\begin{chunk}{axiom.bib}
@article{Lero09,
author = "Leroy, Xavier",
title = {{A Formally Verified Compiler Backend}},
journal = "Logic in Computer Science",
volume = "43",
number = "4",
pages = "363446",
year = "2009",
abstract =
"This article describes the development and formal verificat ion
(proof of semantic preservation) of a compiler backend from Cminor
(a simple imperative intermediate language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its soundness. Such a verified compiler is useful in the
context of formal methods applied to the certification of critical
software: the verification of the compiler guarantees that the safety
properties proved on the source code hold for the executable compiled
code as well.",
paper = "Lero09.pdf"
}
\end{chunk}
\index{Dargaye, Zaynah}
\index{Leroy, Xavier}
\begin{chunk}{axiom.bib}
@article{Darg07,
author = "Dargaye, Zaynah and Leroy, Xavier",
title = {{Mechanized Verification of CPS Transformations}},
journal = "LNCS",
volume = "4790",
pages = "211225",
year = "2007",
abstract =
"Transformation to continuationpassing style (CPS) is often performed
by optimizing compilers for functional programming languages. As part
of the development and proof of correctness of a compiler for the
miniML functional language, we have mechanically verified the
correctness of two CPS transformations for a callbyvalue λ
$\lambda$calculus with nary functions, recursive functions, data
types and patternmatching. The transformations generalize Plotkin’s
original callbyvalue transformation and Danvy and Nielsen’s
optimized transformation, respectively. We used the Coq proof
assistant to formalize the transformations and conduct and check the
proofs. Originalities of this work include the use of bigstep
operational semantics to avoid difficulties with administrative
redexes, and of twosorted de Bruijn indices to avoid difficulties
with $\alpha$conversion.",
paper = "Darg07.pdf"
}
\end{chunk}
\index{Manolios, Panagiotis}
\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@article{Mano03,
author = "Manolios, Panagiotis and Moore, J Strother",
title = {{Partial Functions in ACL2}},
journal = "J. of Automated Reasoning",
volume = "31",
pages = "107127",
year = "2003",
abstract =
"We describe a method for introducing 'partial functions' into ACL2,
that is, functions not defined everywhere. The function 'definitions'
are actually admitted via the encapsulation principle: the new
function symbol is constrained to satisfy the appropriate
equation. This is permitted only when a witness function can be
exhibited, establishing that the constraint is satisfiable. Of
particular interest is the observation that every tail recursive
definition can be witnessed in ACL2. We describe a macro that allows
the convenient introduction of arbitrary tail recursive functions, and
we discuss how such functions can be used to prove theorems about
state machine models without reasoning about “clocks” or counting the
number of steps until termination. Our macro for introducing “partial
functions” also permits a variety of other recursive schemes, and we
briefly illustrate some of them.",
paper = "Mano03.pdf",
keywords = "printed"
}
\end{chunk}
\index{Boyer, Robert S.}
\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@article{Boye75,
author = "Boyer, Robert S. and Moore, J Strother",
title = {{Proving Theorems About LISP Functions}},
journal = "J. ACM",
volume = "22",
number = "1",
pages = "129144",
year = "1975",
abstract =
"Program verification is the idea that properties of programs can be
precisely stated and proved in the mathematical sense. In this paper,
some simple heuristics combining evaluation and mathematical induction
are describe, which the authors have implemented in a program that
automatically proves a wide variety of theorems about recursive LISP
functions. The method the program uses a generate induction formulas
is described at length. The theorems proved by the program include
that REVERSE is its own inverse and that a particular SORT program is
correct. A list of theorems proved by the program is given.",
paper = "Boye75.pdf"
}
\end{chunk}
\index{Gordon, Michael J.C.}
\begin{chunk}{axiom.bib}
@inproceedings{Gord89,
author = "Gordon, Michael J.C.",
title = {{Mechanizing Programming Logics in Higher Order Logic}},
booktitle = "Current Trends in Hardware Verification and Automated
Theorem Proving",
publisher = "Springer",
year = "1989",
abstract =
"Formal reasoning about computer programs can be based directly on the
seman tics of the programming language, or done in a special purpose
logic like Hoare logic. The advantage of the first approach is that
it guarantees that the formal reasoning applies to the language being
used (it is well known, for example, that Hoare's assignment axiom
fails to hold for most programming languages). The advantage of the
second approach is that the proofs can be more direct and natural.
In this paper, an attempt to get the advantages of both approaches
is described. The rules of Hoare logic are mechanically derived
from the semantics of a simple imperative programming language
(using the HOL system). These rules form the basis for a simple
program verifier in which verification conditions are generated by LCF
style tactics whose validations use the derived Hoare rules.
Because Hoare logic is derived, rather than postulated, it is straight
tforw ard to mix seman tic and axiomatic rea soning. It is also
forward to combine the constructs of Hoare logic with other
applicationspecific notations. This is briefly illustrated for
various logical constructs, including termination statements, VDMstyle
`relational' correctness specifications, weakest precondition
statements and dynamic logic formulae.
The theory underlying the work presented here is well known. Our
contribution is to propose a way of mechanizing this theory in a
way that makes certain practical details work out smoothly .",
paper = "Gord89.pdf"
keywords = "printed"
}
\end{chunk}
\index{Guessarian, Irene}
\index{Meseguer, Jose}
\begin{chunk}{axiom.bib}
@article{Gues87,
author = "Guessarian, Irene and Meseguer, Jose",
title = {{On the Axiomatization of 'IfTHENELSE'}},
journal = "SIAM J. Comput.",
volume = "16",
number = "2",
year = "1987",
abstract =
"The equationally complete proof system for "ifthenelse" of Bloom
and Tindell (this Journal, 12 (1983), pp. 677707) is extended to a
complete proof system for manysorted algebras with extra operations,
predicates and equations among those. We give similar completeness
results for continuous algebras and program schemes (infinite trees)
by the methods of algebraic semantics. These extensions provide a
purely equational proof system to prove properties of functional
programs over userdefinable data types.",
paper = "Gues87.pdf"
}
\end{chunk}
\index{Keimel, Klaus}
\index{Plotkin, Gordon D.}
\begin{chunk}{axiom.bib}
@article{Keim09,
author = "Keimel, Klaus and Plotkin, Gordon D.",
title = {{Predicate Transformers for Extended Probability and
NonDeterminism}},
journal = "Math. Struct. in Comp. Science",
volume = "19",
pages = "501539",
year = "2009",
abstract =
"We investigate laws for predicate transformers for the combination of
nondeterministic choice and (extended) probabilistic choice, where
predicates are taken to be functions to the extended nonnegative
reals, or to closed intervals of such reals. These predicate
transformers correspond to state transformers, which are functions to
conical powerdomains, which are the appropriate powerdomains for the
combined forms of nondeterminism. As with standard powerdomains for
nondeterministic choice, these come in three flavours – lower, upper
and (order)convex – so there are also three kinds of predicate
transformers. In order to make the connection, the powerdomains are
first characterised in terms of relevant classes of functionals.
Much of the development is carried out at an abstract level, a kind of
domaintheoretic functional analysis: one considers dcones, which are
dcpos equipped with a module structure over the nonnegative extended
reals, in place of topological vector spaces. Such a development still
needs to be carried out for probabilistic choice per se ; it would
presumably be necessary to work with a notion of convex space rather
than a cone.",
paper = "Keim09.pdf"
}
\end{chunk}
\index{Gordon, Michael J.}
\index{Milner, Arthur j.}
\index{Wadsworth, Christopher P.}
\begin{chunk}{axiom.bib}
@article{Gord79,
author = "Gordon, Michael J. and Milner, Arthur j. and
Wadsworth, Christopher P.",
title = {{Edinburgh LCF, A Mechanised Logic of Computation:
Introduction}},
journal = "LNCS",
volume = "78",
year = "1979"
paper = "Gord79.pdf"
}
\end{chunk}
\index{Gordon, Michael J.}
\index{Milner, Arthur j.}
\index{Wadsworth, Christopher P.}
\begin{chunk}{axiom.bib}
@article{Gord79a,
author = "Gordon, Michael J. and Milner, Arthur j. and
Wadsworth, Christopher P.",
title = {{Edinburgh LCF, A Mechanised Logic of Computation: ML}},
journal = "LNCS",
volume = "78",
year = "1979"
paper = "Gord79a.pdf"
}
\end{chunk}
\index{Gordon, Michael J.}
\index{Milner, Arthur j.}
\index{Wadsworth, Christopher P.}
\begin{chunk}{axiom.bib}
@article{Gord79b,
author = "Gordon, Michael J. and Milner, Arthur j. and
Wadsworth, Christopher P.",
title = {{Edinburgh LCF, A Mechanised Logic of Computation: PPLAMBDA}},
journal = "LNCS",
volume = "78",
year = "1979"
paper = "Gord79b.pdf"
}
\end{chunk}
\index{Lewis, Robert Y.}
\begin{chunk}{axiom.bib}
@article{Lewi17,
author = "Lewis, Robert Y.",
title = {{An Extensible Ad Hoc Interface between Lean and Mathematica}},
journal = "EPTCS",
volume = "262",
pages = "2337",
year = "2017",
abstract =
"We implement a userextensible ad hoc connection between the Lean
proof assistant and the computer algebra system Mathematica. By
reflecting the syntax of each system in the other and providing a
flexible interface for extending translation, our connection allows
for the exchange of arbitrary information between the two systems. We
show how to make use of the Lean metaprogramming framework to verify
certain Mathematica computations, so that the rigor of the proof
assistant is not compromised.",
paper = "Lewi17.pdf",
keywords = "axiomref,printed"
}
\end{chunk}
\index{Clint, M.}
\index{Hoare, C.A.R}
\begin{chunk}{axiom.bib}
@article{Clin72,
author = "Clint, M. and Hoare, C.A.R",
title = {{Program Proving: Jumps and Functions}},
journal = "Acta Informatica",
volume = "1",
pages = "214224",
year = "1972",
abstract =
"Proof methods adequate for a wide range of computer programs have
been expounded in [1] and [2]. This paper develops a method suitable
for programs containing functions, and a certain kind of jump. The
method is illustrated by the proof of a useful and efficient program
for table lookup by logarithmic search.",
paper = "Clin72.pdf"
}
\end{chunk}
\index{Floyd, Robert W.}
\begin{chunk}{axiom.bib}
@article{Floy64,
author = "Floyd, Robert W.",
title = {{Algorithm 245: Treesort}},
journal = "CACM",
volume = "7",
number = "12",
year = "1964",
pages = "701",
paper = "Floy64.pdf"
}
\end{chunk}
\index{Dijkstra, E.W.}
\begin{chunk}{axiom.bib}
@incollection{Dijk72,
author = "Dijkstra, E.W.",
title = {{Notes on Structured Programming}},
booktitle = "Structured Programming",
publisher = "Academic Press",
year = "1972",
pages = "182"
}
\end{chunk}
\index{Hoare, C.A.R}
\begin{chunk}{axiom.bib}
@incollection{Hoar72,
author = "Hoare, C.A.R",
title = {{Notes on Data Structuring}},
booktitle = "Structured Programming",
publisher = "Academic Press",
year = "1972",
pages = "83174"
}
\end{chunk}
\index{Dahl, OleJohan}
\index{Hoare, C.A.R}
\begin{chunk}{axiom.bib}
@incollection{Dahl72,
author = "Dahl, OleJohan and Hoare, C.A.R",
title = {{Hierachical Program Structure}},
booktitle = "Structured Programming",
publisher = "Academic Press",
year = "1972",
pages = "175220""
}
\end{chunk}
\index{Lamport, Leslie}
\import{Owicki, Susan}
\begin{chunk}{axiom.bib}
@article{Lamp81,
author = "Lamport, Leslie and Owicki, Susan",
title = {{Program Logics and Program Verification}},
journal = "LNCS",
volume = "131",
pages = "197199",
year = "1981",
paper = "Lamp81.pdf",
keywords = "printed"
}
\end{chunk}
\index{Glasner, Ingrid}
\index{Loeckx, Jacquest}
\begin{chunk}{axiom.bib}
@article{Glas78,
author = "Glasner, Ingrid and Loeckx, Jacquest",
title = {{A Calculus for Proving Properties of WhilePrograms}},
journal = "LNCS",
volume = "75",
pages = "252281",
year = "19"78,
paper = "Glas78.pdf",,
keywords = "printed"
}
\end{chunk}
\index{Cartwright, Robert}
\index{McCarthy, John}
\begin{chunk}{axiom.bib}
@article{Cart78,
author = "Cartwright, Robert and McCarthy, John",
title = {{Recursive Programs as Functions in a First Order Theory}},
journal = "LNCS",
volume = "75",
pages = "576629",
year = "1978",
abstract =
"Pure Lisp style recursive function programs are represented in a new
way by sentences and schemata of first order logic. This permits easy
and natural proofs of extensional properties of such programs by
methods that generalize structural induction. It also systematizes
known methods such as recursion induction, subgoal induction,
inductive assertions by interpreting them as first order axiom
schemata. We discuss the metatheorems justifying the representation
and techniques for proving facts about specific programs. We also give
a simpler version of the GiSdeIKleene way of representing computable
functions by first order sentences.",
paper = "Cart78.pdf"
}
\end{chunk}
\index{Cartwright, Robert}
\begin{chunk}{axiom.bib}
@phdthesis{Cart76
author = "Cartwright, Robert",
title = {{A Practical Formal Semantic Definition and Verification
System for Typed LISP}},
school = "Stanford Artificial Intelligence Labs",
year = "1976",
abstract =
'Despite the fact that computer scientists have developed a variety of
formal methods for proving computer programs correct, the formal
verification of a nontrivial program is still a formidable
task. Moreover, the notion of proof is so imprecise in most existing
verification systems, that the validity of the proofs generated is
open to question. With an aim toward rectifying these problems, the
research discussed in this dissertation attempts to accomplish the
following objectives:
\begin{enumerate}
\item To develop a programming language which is sufficiently powerful
to express many interesting algorithms clearly and succintly, yet
simple enough to have a tractable formal semantic definition
\item To completely specify both proof theoretic and model theoretic
formal semantics for this language using the simplest possible
abstractions
\item To develop an interactive program verification system for the
language which automatically performs as many of the straightforward
steps in a verification as possible
\end{enumerate}",
paper = "Cart76.pdf",
}
\end{chunk}
\index{O'Donnell, Michael J.}
\begin{chunk}{axiom.bib}
@article{Odon81,
author = "O'Donnell, Michael J.",
title = {{A Critique of the Foundations of Hoarestyle Programming Logics}},
journal = "LNCS",
volume = "131",
pages = "349374",
year = "1981",
abstract =
"Much recent discussion in computing journals has been devoted to
arguments about the feasibility and usefulness of formal
verification methods for increasing confidence in computer
programs. Too little attention has been given to precise criticism
of specific proposed systems for reasoning about programs. Whether
such systems are to be used for formal verification, by hand or
automatically, or as a rigorous foundation for imformal reasoning,
it is essential that they be logically sound. Several popular
rules in the Hoare language are in fact not sound. These rules
have been accepted because they have not been subjected to
sufficiently strong standards of correctness. This paper attempts
to clarify the different technical definitions of correctness of a
logic, to show that only the strongest of these definitions is
acceptable for Hoare logic, and to correct some of the unsound
rules which have appeared in the literature. The corrected rules
are given merely to show that it is possible to do so. Convenient
and elegant rules for reasoning about certain programming
constructs will probably require a more flexible notation than
Hoare's.",
paper = "Odon81.pdf",
keywords = "printed"
}
\end{chunk}
\index{Manna, Zohar}
\index{Waldinger, Richard}
\begin{chunk}{axiom.bib}
@article{Mann78a,
author = "Manna, Zohar and Waldinger, Richard",
title = {{Is 'sometime' sometimes better than 'always'?}},
journal = "CACM",
volume = "21",
number = "2",
year = "1978",
abstract =
"This paper explores a technique for proving the correctness and
termination of programs simultaneously. This approach, the
{\sl intermittentassertion method}, involves documenting the
program with assertions that must be true at some time when
control passes through the corresponding point, but that need not
be true every time. The method, introduced by Burstall, promises
to provide a valuable complement to the more conventional methods.
The intermittentassertion method is presented with a number of
examples of correctness and termination proofs. Some of these
proofs are markedly simpler than their conventional
counterparts. On the other hand, it is shown that a proof of
correctness or termination by any of the conventional techniques
can be rephrased directly as a proof using intermittent
assertions. Finally it is shown how the intermittent assertion
method can be applied to prove the validity of program
transformations and the correctness of continuously operating
systems.",
paper = "Mann78a.pdf, printed"
}
\end{chunk}
\index{Katz, Shmuel}
\index{Manna, Zohar}
\begin{chunk}{axiom.bib}
@article{Katz75,
author = "Katz, Shmuel and Manna, Zohar",
title = {{A Closer Look at Termination}},
journal = "Acta Informatica",
volume = "5",
pages = "333352",
year = "1975",
abstract =
"Several methods for proving that computer programs terminate are
presented and illustrated. The methods considered involve (a)
using the 'noinfinitelydescendingchain' property of
wellfounded sets (Floyd's approach), (b) bounding a counter
associated with each loop ({\sl loop} approach), (c) showing that
some exit of each loop must be taken ({\sl exit} approach), or (d)
inducting on the structure of the data domain (Burstall's
approach). We indicate the relative merit of each method for
proving termination or nontermination as an integral part of an
automatic verification system.",
paper = "Katz75.pdf",
keywords = "printed"
}
\end{chunk}

books/axiom.bib  577 +++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  723 ++++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  673 +++++++++++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1952 insertions(+), 25 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 41cd613..0306710 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 1160,14 +1160,6 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
@book{Gord79,
 author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
 title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
 comment = "Lecture Notes in Computer Science Volume 78",
 publisher = "SpringerVerlag",
 year = "1979"
}

@article{Gons71,
author = "Gonshor, H.",
title = {{Contributions to Genetic Algebras}},
@@ 8423,6 +8415,28 @@ paper = "Brea89.pdf"
paper = "Harp89.pdf"
}
+@article{Katz75,
+ author = "Katz, Shmuel and Manna, Zohar",
+ title = {{A Closer Look at Termination}},
+ journal = "Acta Informatica",
+ volume = "5",
+ pages = "333352",
+ year = "1975",
+ abstract =
+ "Several methods for proving that computer programs terminate are
+ presented and illustrated. The methods considered involve (a)
+ using the 'noinfinitelydescendingchain' property of
+ wellfounded sets (Floyd's approach), (b) bounding a counter
+ associated with each loop ({\sl loop} approach), (c) showing that
+ some exit of each loop must be taken ({\sl exit} approach), or (d)
+ inducting on the structure of the data domain (Burstall's
+ approach). We indicate the relative merit of each method for
+ proving termination or nontermination as an integral part of an
+ automatic verification system.",
+ paper = "Katz75.pdf",
+ keywords = "printed"
+}
+
@book{Lero17,
author = "Leroy, Xavier and Doligez, Damien and Frish, Alain and
Garrigue, Jacques and Remy, Didier and Vouillon, Jerome",
@@ 8528,6 +8542,35 @@ paper = "Brea89.pdf"
paper = "Mann78.pdf, printed"
}
+@article{Mann78a,
+ author = "Manna, Zohar and Waldinger, Richard",
+ title = {{Is 'sometime' sometimes better than 'always'?}},
+ journal = "CACM",
+ volume = "21",
+ number = "2",
+ year = "1978",
+ abstract =
+ "This paper explores a technique for proving the correctness and
+ termination of programs simultaneously. This approach, the
+ {\sl intermittentassertion method}, involves documenting the
+ program with assertions that must be true at some time when
+ control passes through the corresponding point, but that need not
+ be true every time. The method, introduced by Burstall, promises
+ to provide a valuable complement to the more conventional methods.
+
+ The intermittentassertion method is presented with a number of
+ examples of correctness and termination proofs. Some of these
+ proofs are markedly simpler than their conventional
+ counterparts. On the other hand, it is shown that a proof of
+ correctness or termination by any of the conventional techniques
+ can be rephrased directly as a proof using intermittent
+ assertions. Finally it is shown how the intermittent assertion
+ method can be applied to prove the validity of program
+ transformations and the correctness of continuously operating
+ systems.",
+ paper = "Mann78a.pdf, printed"
+}
+
@misc{Mann80,
author = "Manna, Zohar",
title = {{Lectures on the Logic of Computer Programming}},
@@ 8978,6 +9021,29 @@ paper = "Brea89.pdf"
paper = "Scot76.pdf"
}
+@techreport{Site74,
+ author = "Sites, Richard L.",
+ title = {{Some Thoughts on Proving Clean Termination of Programs}},
+ type = "technical report",
+ institution = "Stanford University",
+ number = "STANCS74417",
+ year = "1974",
+ abstract =
+ "Proof of clean termination is a useful subgoal in the process of
+ proving that a program is totally correct. Clean termination means
+ that the program terminates (no infinite loops) and that it does
+ so normally, without any executiontime semantic errors (integer
+ overflow, use of undefined variables, subscript out of range,
+ etc.). In contrast to proofs of correctness, proof of clean
+ termination requires no extensive annotation of a program by a
+ human user, but the proof says nothing about the results
+ calculated by the program, just that whatever it does, it
+ terminates cleanly. Two example proofs are given, of previously
+ published programs: TREESORT3 by Robert Floyd, and SELECT by
+ Ronald L. Revest and Robert Floyd.",
+ paper = "Site74.pdf"
+}
+
@article{Thie17,
author = "Thiemann, Rene and Yamada, Akihisa",
title = {{Polynomial Factorization: Proof Outline}},
@@ 9143,6 +9209,46 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@inproceedings{Bent07,
+ author = "Benton, Nick and Zarfaty, Uri",
+ title = {{Formalizing and Verifying Semantic Type Soundness of a
+ Simple Compiler}},
+ booktitle = "Principles and Practice of Declarative Programming",
+ publisher = "ACM",
+ pages = "112",
+ year = "2007",
+ abstract =
+ "We describe a semantic type soundness result, formalized in the Coq
+ proof assistant, for a compiler from a simple imperative language with
+ heapallocated data into an idealized assembly language. Types in the
+ highlevel language are interpreted as binary relations, built using
+ both secondorder quantification and a form of separation structure,
+ over stores and code pointers in the lowlevel machine.",
+ paper = "Bent07.pdf",
+ keywords = "printed"
+}
+
+@article{Boye75,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Proving Theorems About LISP Functions}},
+ journal = "J. ACM",
+ volume = "22",
+ number = "1",
+ pages = "129144",
+ year = "1975",
+ abstract =
+ "Program verification is the idea that properties of programs can be
+ precisely stated and proved in the mathematical sense. In this paper,
+ some simple heuristics combining evaluation and mathematical induction
+ are describe, which the authors have implemented in a program that
+ automatically proves a wide variety of theorems about recursive LISP
+ functions. The method the program uses a generate induction formulas
+ is described at length. The theorems proved by the program include
+ that REVERSE is its own inverse and that a particular SORT program is
+ correct. A list of theorems proved by the program is given.",
+ paper = "Boye75.pdf"
+}
+
@inproceedings{Cald97,
author = "Caldwell, James L.",
title = {{Moving proofsasprograms into practice}},
@@ 9167,6 +9273,149 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@phdthesis{Cart76,
+ author = "Cartwright, Robert",
+ title = {{A Practical Formal Semantic Definition and Verification
+ System for Typed LISP}},
+ school = "Stanford Artificial Intelligence Labs",
+ year = "1976",
+ abstract =
+ "Despite the fact that computer scientists have developed a variety of
+ formal methods for proving computer programs correct, the formal
+ verification of a nontrivial program is still a formidable
+ task. Moreover, the notion of proof is so imprecise in most existing
+ verification systems, that the validity of the proofs generated is
+ open to question. With an aim toward rectifying these problems, the
+ research discussed in this dissertation attempts to accomplish the
+ following objectives:
+ \begin{enumerate}
+ \item To develop a programming language which is sufficiently powerful
+ to express many interesting algorithms clearly and succintly, yet
+ simple enough to have a tractable formal semantic definition
+ \item To completely specify both proof theoretic and model theoretic
+ formal semantics for this language using the simplest possible
+ abstractions
+ \item To develop an interactive program verification system for the
+ language which automatically performs as many of the straightforward
+ steps in a verification as possible
+ \end{enumerate}",
+ paper = "Cart76.pdf",
+}
+
+@article{Cart78,
+ author = "Cartwright, Robert and McCarthy, John",
+ title = {{Recursive Programs as Functions in a First Order Theory}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "576629",
+ year = "1978",
+ abstract =
+ "Pure Lisp style recursive function programs are represented in a new
+ way by sentences and schemata of first order logic. This permits easy
+ and natural proofs of extensional properties of such programs by
+ methods that generalize structural induction. It also systematizes
+ known methods such as recursion induction, subgoal induction,
+ inductive assertions by interpreting them as first order axiom
+ schemata. We discuss the metatheorems justifying the representation
+ and techniques for proving facts about specific programs. We also give
+ a simpler version of the GiSdeIKleene way of representing computable
+ functions by first order sentences.",
+ paper = "Cart78.pdf"
+}
+
+@article{Chli07,
+ author = "Chlipala, Adam J.",
+ title = {{A Certified TypePreserving Compiler from the Lambda Calculus
+ to Assembly Language}},
+ journal = "ACM SIGPLAN PLDI'07",
+ volume = "42",
+ number = "6",
+ year = "2007",
+ pages = "5465",
+ abstract =
+ "We present a certified compiler from the simplytyped lambda calculus
+ to assembly language. The compiler is certified in the sense that it
+ comes with a machinechecked proof of semantics preservation,
+ performed with the Coq proof assistant. The compiler and the terms of
+ its several intermediate languages are given dependent types that
+ guarantee that only welltyped programs are representable. Thus, type
+ preservation for each compiler pass follows without any significant
+ 'proofs' of the usual kind. Semantics preservation is proved based on
+ denotational semantics assigned to the intermediate languages. We
+ demonstrate how working with a typepreserving compiler enables
+ typedirected proof search to discharge large parts of our proof
+ obligations automatically.",
+ paper = "Chli07.pdf"
+}
+
+@article{Clin72,
+ author = "Clint, M. and Hoare, C.A.R",
+ title = {{Program Proving: Jumps and Functions}},
+ journal = "Acta Informatica",
+ volume = "1",
+ pages = "214224",
+ year = "1972",
+ abstract =
+ "Proof methods adequate for a wide range of computer programs have
+ been expounded in [1] and [2]. This paper develops a method suitable
+ for programs containing functions, and a certain kind of jump. The
+ method is illustrated by the proof of a useful and efficient program
+ for table lookup by logarithmic search.",
+ paper = "Clin72.pdf"
+}
+
+@misc{Crar08,
+ author = "Crary, Karl and Sarkar, Susmit",
+ title = {{Foundational Certified Code in a Metalogical Framework}},
+ link = "\url{http://repository.cmu.edu/compsci/470/}",
+ year = "2008",
+ abstract =
+ "Foundational certified code systems seek to prove untrusted programs
+ to be safe relative to safety policies given in terms of actual
+ machine architectures, thereby improving the systems' flexibility and
+ extensibility. Using the Twelf metalogical framework, we have
+ constructed a safety policy for the IA32 architecture with a trusted
+ runtime library. The safety policy is based on a formalized
+ operational semantics. We have also developed a complete, foundational
+ proof that a fully expressive typed assembly language satisfies that
+ safety policy",
+ paper = "Crar08.pdf"
+}
+
+@incollection{Dahl72,
+ author = "Dahl, OleJohan and Hoare, C.A.R",
+ title = {{Hierachical Program Structure}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "175220"
+}
+
+@article{Darg07,
+ author = "Dargaye, Zaynah and Leroy, Xavier",
+ title = {{Mechanized Verification of CPS Transformations}},
+ journal = "LNCS",
+ volume = "4790",
+ pages = "211225",
+ year = "2007",
+ abstract =
+ "Transformation to continuationpassing style (CPS) is often performed
+ by optimizing compilers for functional programming languages. As part
+ of the development and proof of correctness of a compiler for the
+ miniML functional language, we have mechanically verified the
+ correctness of two CPS transformations for a callbyvalue λ
+ $\lambda$calculus with nary functions, recursive functions, data
+ types and patternmatching. The transformations generalize Plotkin’s
+ original callbyvalue transformation and Danvy and Nielsen’s
+ optimized transformation, respectively. We used the Coq proof
+ assistant to formalize the transformations and conduct and check the
+ proofs. Originalities of this work include the use of bigstep
+ operational semantics to avoid difficulties with administrative
+ redexes, and of twosorted de Bruijn indices to avoid difficulties
+ with $\alpha$conversion.",
+ paper = "Darg07.pdf"
+}
+
@phdthesis{Davi09,
author = "Davis, Jared Curran",
title = {{A SelfVerifying Theorem Prover}},
@@ 9243,6 +9492,15 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@incollection{Dijk72a,
+ author = "Dijkstra, E.W.",
+ title = {{Notes on Structured Programming}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "182"
+}
+
@misc{Domi18,
author = "Domipheus",
title = {{Designing a CPU in VHDL}},
@@ 9310,6 +9568,17 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Floy64,
+ author = "Floyd, Robert W.",
+ title = {{Algorithm 245: Treesort}},
+ journal = "CACM",
+ volume = "7",
+ number = "12",
+ year = "1964",
+ pages = "701",
+ paper = "Floy64.pdf"
+}
+
@inproceedings{Floy67,
author = "Floyd, Robert W.",
title = {{Assigning Meanings to Programs}},
@@ 9321,6 +9590,223 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Foxx03,
+ author = "Fox, Anthony",
+ title = {{Formal Specification and Verification of ARM6}},
+ journal = "LNCS",
+ volume = "2758",
+ pages = "2540",
+ year = "2003",
+ abstract =
+ "This paper gives an overview of progress made on the formal
+ specification and verification of the ARM6 microarchitecture using
+ the HOL proof system. The ARM6 is a commercial processor design preva
+ lent in mobile and embedded systems – it features a 3stage pipeline
+ with a multicycle execute stage, six operating modes and a rich
+ 32bit RISC instruction set. This paper describes some of the
+ difficulties encountered when working with a full blown instruction
+ set architecture that has not been designed with verification in mind.",
+ paper = "Foxx03.pdf"
+}
+
+@article{Glas78,
+ author = "Glasner, Ingrid and Loeckx, Jacquest",
+ title = {{A Calculus for Proving Properties of WhilePrograms}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "252281",
+ year = "1978",
+ paper = "Glas78.pdf",
+ keywords = "printed"
+}
+
+@article{Gord79,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation:
+ Introduction}},
+ publisher = "SpringerVerlag",
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79.pdf"
+}
+
+@article{Gord79a,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: ML}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79a.pdf"
+}
+
+@article{Gord79b,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: PPLAMBDA}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79b.pdf"
+}
+
+@inproceedings{Gord89,
+ author = "Gordon, Michael J.C.",
+ title = {{Mechanizing Programming Logics in Higher Order Logic}},
+ booktitle = "Current Trends in Hardware Verification and Automated
+ Theorem Proving",
+ publisher = "Springer",
+ year = "1989",
+ abstract =
+ "Formal reasoning about computer programs can be based directly on the
+ seman tics of the programming language, or done in a special purpose
+ logic like Hoare logic. The advantage of the first approach is that
+ it guarantees that the formal reasoning applies to the language being
+ used (it is well known, for example, that Hoare's assignment axiom
+ fails to hold for most programming languages). The advantage of the
+ second approach is that the proofs can be more direct and natural.
+
+ In this paper, an attempt to get the advantages of both approaches
+ is described. The rules of Hoare logic are mechanically derived
+ from the semantics of a simple imperative programming language
+ (using the HOL system). These rules form the basis for a simple
+ program verifier in which verification conditions are generated by LCF
+ style tactics whose validations use the derived Hoare rules.
+ Because Hoare logic is derived, rather than postulated, it is straight
+ tforw ard to mix seman tic and axiomatic rea soning. It is also
+ forward to combine the constructs of Hoare logic with other
+ applicationspecific notations. This is briefly illustrated for
+ various logical constructs, including termination statements, VDMstyle
+ `relational' correctness specifications, weakest precondition
+ statements and dynamic logic formulae.
+
+ The theory underlying the work presented here is well known. Our
+ contribution is to propose a way of mechanizing this theory in a
+ way that makes certain practical details work out smoothly .",
+ paper = "Gord89.pdf",
+ keywords = "printed"
+}
+
+@article{Gord06,
+ author = "Gordon, Mike and Iyoda, Juliano and Owens, Scott and
+ Slind, Konrad",
+ title = {{Automatic Formal Synthesis of Hardware from Higher Order Logic}},
+ journal = "Electronic Notes in Theoretical Computer Science",
+ volume = "145",
+ pages = "2743",
+ year = "2006",
+ abstract =
+ "A compiler that automatically translates recursive function
+ definitions in higher order logic to clocked synchronous hardware is
+ described. Compilation is by mechanised proof in the HOL4 system, and
+ generates a correctness theorem for each function that is
+ compiled. Logic formulas representing circuits are synthesised in a
+ form suitable for direct translation to Verilog HDL for simulation and
+ input to standard design automation tools. The compilation scripts are
+ open and can be safely modified: synthesised circuits are
+ correctbyconstruction. The synthesisable subset of higher order
+ logic can be extended using additional proofbased tools that
+ transform definitions into the subset.",
+ paper = "Gord06.pdf"
+}
+
+@article{Gutt95,
+ author = "Guttman, Joshua D. and Ramsdell, John D. and Wand, Mitchell",
+ title = {{VLISP: A Verified Implementation of Scheme}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "8",
+ pages = "532",
+ year = "1995",
+ abstract =
+ "The VL!SP project showed how to produce a comprehensively verified
+ implementation for a programming language, namely Scheme. This paper
+ introduces two more detailed studies on VLISP [13, 21). It summarizes
+ the basic techniques that were used repeatedly throughout the effort.
+ It presents scientific conclusions about the applicability of the
+ these techniques as well as engineering conclusions about the crucial
+ choices that allowed the verification to succeed.",
+ paper = "Gutt95.pdf"
+}
+
+@incollection{Hoar72,
+ author = "Hoare, C.A.R",
+ title = {{Notes on Data Structuring}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "83174"
+}
+
+@article{Keim09,
+ author = "Keimel, Klaus and Plotkin, Gordon D.",
+ title = {{Predicate Transformers for Extended Probability and
+ NonDeterminism}},
+ journal = "Math. Struct. in Comp. Science",
+ volume = "19",
+ pages = "501539",
+ year = "2009",
+ abstract =
+ "We investigate laws for predicate transformers for the combination of
+ nondeterministic choice and (extended) probabilistic choice, where
+ predicates are taken to be functions to the extended nonnegative
+ reals, or to closed intervals of such reals. These predicate
+ transformers correspond to state transformers, which are functions to
+ conical powerdomains, which are the appropriate powerdomains for the
+ combined forms of nondeterminism. As with standard powerdomains for
+ nondeterministic choice, these come in three flavours – lower, upper
+ and (order)convex – so there are also three kinds of predicate
+ transformers. In order to make the connection, the powerdomains are
+ first characterised in terms of relevant classes of functionals.
+
+ Much of the development is carried out at an abstract level, a kind of
+ domaintheoretic functional analysis: one considers dcones, which are
+ dcpos equipped with a module structure over the nonnegative extended
+ reals, in place of topological vector spaces. Such a development still
+ needs to be carried out for probabilistic choice per se ; it would
+ presumably be necessary to work with a notion of convex space rather
+ than a cone.",
+ paper = "Keim09.pdf"
+}
+
+@article{Lamp81,
+ author = "Lamport, Leslie and Owicki, Susan",
+ title = {{Program Logics and Program Verification}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "197199",
+ year = "1981",
+ paper = "Lamp81.pdf",
+ keywords = "printed"
+}
+
+@article{Mano03,
+ author = "Manolios, Panagiotis and Moore, J Strother",
+ title = {{Partial Functions in ACL2}},
+ journal = "J. of Automated Reasoning",
+ volume = "31",
+ pages = "107127",
+ year = "2003",
+ abstract =
+ "We describe a method for introducing 'partial functions' into ACL2,
+ that is, functions not defined everywhere. The function 'definitions'
+ are actually admitted via the encapsulation principle: the new
+ function symbol is constrained to satisfy the appropriate
+ equation. This is permitted only when a witness function can be
+ exhibited, establishing that the constraint is satisfiable. Of
+ particular interest is the observation that every tail recursive
+ definition can be witnessed in ACL2. We describe a macro that allows
+ the convenient introduction of arbitrary tail recursive functions, and
+ we discuss how such functions can be used to prove theorems about
+ state machine models without reasoning about “clocks” or counting the
+ number of steps until termination. Our macro for introducing “partial
+ functions” also permits a variety of other recursive schemes, and we
+ briefly illustrate some of them.",
+ paper = "Mano03.pdf",
+ keywords = "printed"
+}
+
@book{Morg98,
author = "Morgan, Carroll",
title = {{Programming from Specifcations, 2nd Ed.}},
@@ 9472,6 +9958,37 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Odon81,
+ author = "O'Donnell, Michael J.",
+ title = {{A Critique of the Foundations of Hoarestyle Programming Logics}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "349374",
+ year = "1981",
+ abstract =
+ "Much recent discussion in computing journals has been devoted to
+ arguments about the feasibility and usefulness of formal
+ verification methods for increasing confidence in computer
+ programs. Too little attention has been given to precise criticism
+ of specific proposed systems for reasoning about programs. Whether
+ such systems are to be used for formal verification, by hand or
+ automatically, or as a rigorous foundation for imformal reasoning,
+ it is essential that they be logically sound. Several popular
+ rules in the Hoare language are in fact not sound. These rules
+ have been accepted because they have not been subjected to
+ sufficiently strong standards of correctness. This paper attempts
+ to clarify the different technical definitions of correctness of a
+ logic, to show that only the strongest of these definitions is
+ acceptable for Hoare logic, and to correct some of the unsound
+ rules which have appeared in the literature. The corrected rules
+ are given merely to show that it is possible to do so. Convenient
+ and elegant rules for reasoning about certain programming
+ constructs will probably require a more flexible notation than
+ Hoare's.",
+ paper = "Odon81.pdf",
+ keywords = "printed"
+}
+
@inproceedings{Talp92,
author = "Talpin, JeanPierre and Jouvelot, Pierre",
title = {{The Type and Effect Discipline}},
@@ 9500,6 +10017,27 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Lero09,
+ author = "Leroy, Xavier",
+ title = {{A Formally Verified Compiler Backend}},
+ journal = "Logic in Computer Science",
+ volume = "43",
+ number = "4",
+ pages = "363446",
+ year = "2009",
+ abstract =
+ "This article describes the development and formal verification
+ (proof of semantic preservation) of a compiler backend from Cminor
+ (a simple imperative intermediate language) to PowerPC assembly code,
+ using the Coq proof assistant both for programming the compiler and
+ for proving its soundness. Such a verified compiler is useful in the
+ context of formal methods applied to the certification of critical
+ software: the verification of the compiler guarantees that the safety
+ properties proved on the source code hold for the executable compiled
+ code as well.",
+ paper = "Lero09.pdf"
+}
+
@incollection{Soze06,
author = "Sozeau, Matthieu",
title = {{Subset Coercions in Coq}},
@@ 14510,7 +15048,8 @@ paper = "Brea89.pdf"
must have some personal experience of understanding to attain
belief, and to have this experience you must engage your intuition
and other mental processes which are impossible to formalise.",
 paper = "Poll97.pdf"
+ paper = "Poll97.pdf",
+ keywords = "printed"
}
@article{Prev02,
@@ 30887,6 +31426,26 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Lewi17,
+ author = "Lewis, Robert Y.",
+ title = {{An Extensible Ad Hoc Interface between Lean and Mathematica}},
+ journal = "EPTCS",
+ volume = "262",
+ pages = "2337",
+ year = "2017",
+ abstract =
+ "We implement a userextensible ad hoc connection between the Lean
+ proof assistant and the computer algebra system Mathematica. By
+ reflecting the syntax of each system in the other and providing a
+ flexible interface for extending translation, our connection allows
+ for the exchange of arbitrary information between the two systems. We
+ show how to make use of the Lean metaprogramming framework to verify
+ certain Mathematica computations, so that the rigor of the proof
+ assistant is not compromised.",
+ paper = "Lewi17.pdf",
+ keywords = "axiomref,printed"
+}
+
@inproceedings{Liao95,
author = "Liao, HsinChao and Fateman, Richard J.",
title = {{Evaluation of the heuristic polynomial GCD}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index dc68b61..d365b2a 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 1757,20 +1757,6 @@ paper = "Brea89.pdf"
\end{chunk}
\index{Gordon, M.}
\index{Milner, R.}
\index{Wadsworth, C.P.}
\begin{chunk}{axiom.bib}
@book{Gord79,
 author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
 title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
 comment = "Lecture Notes in Computer Science Volume 78",
 publisher = "SpringerVerlag",
 year = "1979"
}

\end{chunk}

\index{Gonshor, H.}
\index{AlgebraGivenByStructuralConstants}
\begin{chunk}{axiom.bib}
@@ 11265,6 +11251,33 @@ when shown in factored form.
\end{chunk}
+\index{Katz, Shmuel}
+\index{Manna, Zohar}
+\begin{chunk}{axiom.bib}
+@article{Katz75,
+ author = "Katz, Shmuel and Manna, Zohar",
+ title = {{A Closer Look at Termination}},
+ journal = "Acta Informatica",
+ volume = "5",
+ pages = "333352",
+ year = "1975",
+ abstract =
+ "Several methods for proving that computer programs terminate are
+ presented and illustrated. The methods considered involve (a)
+ using the 'noinfinitelydescendingchain' property of
+ wellfounded sets (Floyd's approach), (b) bounding a counter
+ associated with each loop ({\sl loop} approach), (c) showing that
+ some exit of each loop must be taken ({\sl exit} approach), or (d)
+ inducting on the structure of the data domain (Burstall's
+ approach). We indicate the relative merit of each method for
+ proving termination or nontermination as an integral part of an
+ automatic verification system.",
+ paper = "Katz75.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Leroy, Xavier}
\index{Doligez, Damien}
\index{Frish, Alain}
@@ 11402,6 +11415,40 @@ when shown in factored form.
\end{chunk}
\index{Manna, Zohar}
+\index{Waldinger, Richard}
+\begin{chunk}{axiom.bib}
+@article{Mann78a,
+ author = "Manna, Zohar and Waldinger, Richard",
+ title = {{Is 'sometime' sometimes better than 'always'?}},
+ journal = "CACM",
+ volume = "21",
+ number = "2",
+ year = "1978",
+ abstract =
+ "This paper explores a technique for proving the correctness and
+ termination of programs simultaneously. This approach, the
+ {\sl intermittentassertion method}, involves documenting the
+ program with assertions that must be true at some time when
+ control passes through the corresponding point, but that need not
+ be true every time. The method, introduced by Burstall, promises
+ to provide a valuable complement to the more conventional methods.
+
+ The intermittentassertion method is presented with a number of
+ examples of correctness and termination proofs. Some of these
+ proofs are markedly simpler than their conventional
+ counterparts. On the other hand, it is shown that a proof of
+ correctness or termination by any of the conventional techniques
+ can be rephrased directly as a proof using intermittent
+ assertions. Finally it is shown how the intermittent assertion
+ method can be applied to prove the validity of program
+ transformations and the correctness of continuously operating
+ systems.",
+ paper = "Mann78a.pdf, printed"
+}
+
+\end{chunk}
+
+\index{Manna, Zohar}
\begin{chunk}{axiom.bib}
@misc{Mann80,
author = "Manna, Zohar",
@@ 11939,6 +11986,33 @@ when shown in factored form.
\end{chunk}
+\index{Sites, Richard L.}
+\begin{chunk}{axiom.bib}
+@techreport{Site74,
+ author = "Sites, Richard L.",
+ title = {{Some Thoughts on Proving Clean Termination of Programs}},
+ type = "technical report",
+ institution = "Stanford University",
+ number = "STANCS74417",
+ year = "1974",
+ abstract =
+ "Proof of clean termination is a useful subgoal in the process of
+ proving that a program is totally correct. Clean termination means
+ that the program terminates (no infinite loops) and that it does
+ so normally, without any executiontime semantic errors (integer
+ overflow, use of undefined variables, subscript out of range,
+ etc.). In contrast to proofs of correctness, proof of clean
+ termination requires no extensive annotation of a program by a
+ human user, but the proof says nothing about the results
+ calculated by the program, just that whatever it does, it
+ terminates cleanly. Two example proofs are given, of previously
+ published programs: TREESORT3 by Robert Floyd, and SELECT by
+ Ronald L. Revest and Robert Floyd.",
+ paper = "Site74.pdf"
+}
+
+\end{chunk}
+
\index{Thiemann, Rene}
\index{Yamada, Akihisa}
\begin{chunk}{axiom.bib}
@@ 12153,6 +12227,56 @@ when shown in factored form.
\end{chunk}
+\index{Benton, Nick}
+\index{Zarfaty, Uri}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bent07,
+ author = "Benton, Nick and Zarfaty, Uri",
+ title = {{Formalizing and Verifying Semantic Type Soundness of a
+ Simple Compiler}},
+ booktitle = "Principles and Practice of Declarative Programming",
+ publisher = "ACM",
+ pages = "112",
+ year = "2007",
+ abstract =
+ "We describe a semantic type soundness result, formalized in the Coq
+ proof assistant, for a compiler from a simple imperative language with
+ heapallocated data into an idealized assembly language. Types in the
+ highlevel language are interpreted as binary relations, built using
+ both secondorder quantification and a form of separation structure,
+ over stores and code pointers in the lowlevel machine.",
+ paper = "Bent07.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Boyer, Robert S.}
+\index{Moore, J Strother}
+\begin{chunk}{axiom.bib}
+@article{Boye75,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Proving Theorems About LISP Functions}},
+ journal = "J. ACM",
+ volume = "22",
+ number = "1",
+ pages = "129144",
+ year = "1975",
+ abstract =
+ "Program verification is the idea that properties of programs can be
+ precisely stated and proved in the mathematical sense. In this paper,
+ some simple heuristics combining evaluation and mathematical induction
+ are describe, which the authors have implemented in a program that
+ automatically proves a wide variety of theorems about recursive LISP
+ functions. The method the program uses a generate induction formulas
+ is described at length. The theorems proved by the program include
+ that REVERSE is its own inverse and that a particular SORT program is
+ correct. A list of theorems proved by the program is given.",
+ paper = "Boye75.pdf"
+}
+
+\end{chunk}
+
\index{Caldwell, James L.}
\begin{chunk}{axiom.bib}
@inproceedings{Cald97,
@@ 12181,6 +12305,182 @@ when shown in factored form.
\end{chunk}
+\index{Cartwright, Robert}
+\begin{chunk}{axiom.bib}
+@phdthesis{Cart76,
+ author = "Cartwright, Robert",
+ title = {{A Practical Formal Semantic Definition and Verification
+ System for Typed LISP}},
+ school = "Stanford Artificial Intelligence Labs",
+ year = "1976",
+ abstract =
+ "Despite the fact that computer scientists have developed a variety of
+ formal methods for proving computer programs correct, the formal
+ verification of a nontrivial program is still a formidable
+ task. Moreover, the notion of proof is so imprecise in most existing
+ verification systems, that the validity of the proofs generated is
+ open to question. With an aim toward rectifying these problems, the
+ research discussed in this dissertation attempts to accomplish the
+ following objectives:
+ \begin{enumerate}
+ \item To develop a programming language which is sufficiently powerful
+ to express many interesting algorithms clearly and succintly, yet
+ simple enough to have a tractable formal semantic definition
+ \item To completely specify both proof theoretic and model theoretic
+ formal semantics for this language using the simplest possible
+ abstractions
+ \item To develop an interactive program verification system for the
+ language which automatically performs as many of the straightforward
+ steps in a verification as possible
+ \end{enumerate}",
+ paper = "Cart76.pdf",
+}
+
+\end{chunk}
+
+\index{Cartwright, Robert}
+\index{McCarthy, John}
+\begin{chunk}{axiom.bib}
+@article{Cart78,
+ author = "Cartwright, Robert and McCarthy, John",
+ title = {{Recursive Programs as Functions in a First Order Theory}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "576629",
+ year = "1978",
+ abstract =
+ "Pure Lisp style recursive function programs are represented in a new
+ way by sentences and schemata of first order logic. This permits easy
+ and natural proofs of extensional properties of such programs by
+ methods that generalize structural induction. It also systematizes
+ known methods such as recursion induction, subgoal induction,
+ inductive assertions by interpreting them as first order axiom
+ schemata. We discuss the metatheorems justifying the representation
+ and techniques for proving facts about specific programs. We also give
+ a simpler version of the GiSdeIKleene way of representing computable
+ functions by first order sentences.",
+ paper = "Cart78.pdf"
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam J.}
+\begin{chunk}{axiom.bib}
+@article{Chli07,
+ author = "Chlipala, Adam J.",
+ title = {{A Certified TypePreserving Compiler from the Lambda Calculus
+ to Assembly Language}},
+ journal = "ACM SIGPLAN PLDI'07",
+ volume = "42",
+ number = "6",
+ year = "2007",
+ pages = "5465",
+ abstract =
+ "We present a certified compiler from the simplytyped lambda calculus
+ to assembly language. The compiler is certified in the sense that it
+ comes with a machinechecked proof of semantics preservation,
+ performed with the Coq proof assistant. The compiler and the terms of
+ its several intermediate languages are given dependent types that
+ guarantee that only welltyped programs are representable. Thus, type
+ preservation for each compiler pass follows without any significant
+ 'proofs' of the usual kind. Semantics preservation is proved based on
+ denotational semantics assigned to the intermediate languages. We
+ demonstrate how working with a typepreserving compiler enables
+ typedirected proof search to discharge large parts of our proof
+ obligations automatically.",
+ paper = "Chli07.pdf"
+}
+
+\end{chunk}
+
+\index{Clint, M.}
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@article{Clin72,
+ author = "Clint, M. and Hoare, C.A.R",
+ title = {{Program Proving: Jumps and Functions}},
+ journal = "Acta Informatica",
+ volume = "1",
+ pages = "214224",
+ year = "1972",
+ abstract =
+ "Proof methods adequate for a wide range of computer programs have
+ been expounded in [1] and [2]. This paper develops a method suitable
+ for programs containing functions, and a certain kind of jump. The
+ method is illustrated by the proof of a useful and efficient program
+ for table lookup by logarithmic search.",
+ paper = "Clin72.pdf"
+}
+
+\end{chunk}
+
+\index{Crary, Karl}
+\index{Sarkar, Susmit}
+\begin{chunk}{axiom.bib}
+@misc{Crar08,
+ author = "Crary, Karl and Sarkar, Susmit",
+ title = {{Foundational Certified Code in a Metalogical Framework}},
+ link = "\url{http://repository.cmu.edu/compsci/470/}",
+ year = "2008",
+ abstract =
+ "Foundational certified code systems seek to prove untrusted programs
+ to be safe relative to safety policies given in terms of actual
+ machine architectures, thereby improving the systems' flexibility and
+ extensibility. Using the Twelf metalogical framework, we have
+ constructed a safety policy for the IA32 architecture with a trusted
+ runtime library. The safety policy is based on a formalized
+ operational semantics. We have also developed a complete, foundational
+ proof that a fully expressive typed assembly language satisfies that
+ safety policy",
+ paper = "Crar08.pdf"
+}
+
+\end{chunk}
+
+\index{Dahl, OleJohan}
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@incollection{Dahl72,
+ author = "Dahl, OleJohan and Hoare, C.A.R",
+ title = {{Hierachical Program Structure}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "175220"
+}
+
+\end{chunk}
+
+\index{Dargaye, Zaynah}
+\index{Leroy, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Darg07,
+ author = "Dargaye, Zaynah and Leroy, Xavier",
+ title = {{Mechanized Verification of CPS Transformations}},
+ journal = "LNCS",
+ volume = "4790",
+ pages = "211225",
+ year = "2007",
+ abstract =
+ "Transformation to continuationpassing style (CPS) is often performed
+ by optimizing compilers for functional programming languages. As part
+ of the development and proof of correctness of a compiler for the
+ miniML functional language, we have mechanically verified the
+ correctness of two CPS transformations for a callbyvalue λ
+ $\lambda$calculus with nary functions, recursive functions, data
+ types and patternmatching. The transformations generalize Plotkin’s
+ original callbyvalue transformation and Danvy and Nielsen’s
+ optimized transformation, respectively. We used the Coq proof
+ assistant to formalize the transformations and conduct and check the
+ proofs. Originalities of this work include the use of bigstep
+ operational semantics to avoid difficulties with administrative
+ redexes, and of twosorted de Bruijn indices to avoid difficulties
+ with $\alpha$conversion.",
+ paper = "Darg07.pdf"
+}
+
+\end{chunk}
+
\index{Davis, Jared Curran}
\begin{chunk}{axiom.bib}
@phdthesis{Davi09,
@@ 12266,6 +12566,19 @@ when shown in factored form.
\end{chunk}
+\index{Dijkstra, E.W.}
+\begin{chunk}{axiom.bib}
+@incollection{Dijk72a,
+ author = "Dijkstra, E.W.",
+ title = {{Notes on Structured Programming}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "182"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Domi18,
author = "Domipheus",
@@ 12347,6 +12660,21 @@ when shown in factored form.
\index{Floyd, Robert W.}
\begin{chunk}{axiom.bib}
+@article{Floy64,
+ author = "Floyd, Robert W.",
+ title = {{Algorithm 245: Treesort}},
+ journal = "CACM",
+ volume = "7",
+ number = "12",
+ year = "1964",
+ pages = "701",
+ paper = "Floy64.pdf"
+}
+
+\end{chunk}
+
+\index{Floyd, Robert W.}
+\begin{chunk}{axiom.bib}
@inproceedings{Floy67,
author = "Floyd, Robert W.",
title = {{Assigning Meanings to Programs}},
@@ 12360,6 +12688,286 @@ when shown in factored form.
\end{chunk}
+\index{Fox, Anthony}
+\begin{chunk}{axiom.bib}
+@article{Foxx03,
+ author = "Fox, Anthony",
+ title = {{Formal Specification and Verification of ARM6}},
+ journal = "LNCS",
+ volume = "2758",
+ pages = "2540",
+ year = "2003",
+ abstract =
+ "This paper gives an overview of progress made on the formal
+ specification and verification of the ARM6 microarchitecture using
+ the HOL proof system. The ARM6 is a commercial processor design preva
+ lent in mobile and embedded systems – it features a 3stage pipeline
+ with a multicycle execute stage, six operating modes and a rich
+ 32bit RISC instruction set. This paper describes some of the
+ difficulties encountered when working with a full blown instruction
+ set architecture that has not been designed with verification in mind.",
+ paper = "Foxx03.pdf"
+}
+
+\end{chunk}
+
+\index{Glasner, Ingrid}
+\index{Loeckx, Jacquest}
+\begin{chunk}{axiom.bib}
+@article{Glas78,
+ author = "Glasner, Ingrid and Loeckx, Jacquest",
+ title = {{A Calculus for Proving Properties of WhilePrograms}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "252281",
+ year = "1978",
+ paper = "Glas78.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation:
+ Introduction}},
+ publisher = "SpringerVerlag",
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79a,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: ML}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79a.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79b,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: PPLAMBDA}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979",
+ paper = "Gord79b.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.C.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gord89,
+ author = "Gordon, Michael J.C.",
+ title = {{Mechanizing Programming Logics in Higher Order Logic}},
+ booktitle = "Current Trends in Hardware Verification and Automated
+ Theorem Proving",
+ publisher = "Springer",
+ year = "1989",
+ abstract =
+ "Formal reasoning about computer programs can be based directly on the
+ seman tics of the programming language, or done in a special purpose
+ logic like Hoare logic. The advantage of the first approach is that
+ it guarantees that the formal reasoning applies to the language being
+ used (it is well known, for example, that Hoare's assignment axiom
+ fails to hold for most programming languages). The advantage of the
+ second approach is that the proofs can be more direct and natural.
+
+ In this paper, an attempt to get the advantages of both approaches
+ is described. The rules of Hoare logic are mechanically derived
+ from the semantics of a simple imperative programming language
+ (using the HOL system). These rules form the basis for a simple
+ program verifier in which verification conditions are generated by LCF
+ style tactics whose validations use the derived Hoare rules.
+ Because Hoare logic is derived, rather than postulated, it is straight
+ tforw ard to mix seman tic and axiomatic rea soning. It is also
+ forward to combine the constructs of Hoare logic with other
+ applicationspecific notations. This is briefly illustrated for
+ various logical constructs, including termination statements, VDMstyle
+ `relational' correctness specifications, weakest precondition
+ statements and dynamic logic formulae.
+
+ The theory underlying the work presented here is well known. Our
+ contribution is to propose a way of mechanizing this theory in a
+ way that makes certain practical details work out smoothly .",
+ paper = "Gord89.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Gordon, Mike}
+\index{Iyoda, Juliano}
+\index{Owens, Scott}
+\index{Slind, Konrad}
+\begin{chunk}{axiom.bib}
+@article{Gord06,
+ author = "Gordon, Mike and Iyoda, Juliano and Owens, Scott and
+ Slind, Konrad",
+ title = {{Automatic Formal Synthesis of Hardware from Higher Order Logic}},
+ journal = "Electronic Notes in Theoretical Computer Science",
+ volume = "145",
+ pages = "2743",
+ year = "2006",
+ abstract =
+ "A compiler that automatically translates recursive function
+ definitions in higher order logic to clocked synchronous hardware is
+ described. Compilation is by mechanised proof in the HOL4 system, and
+ generates a correctness theorem for each function that is
+ compiled. Logic formulas representing circuits are synthesised in a
+ form suitable for direct translation to Verilog HDL for simulation and
+ input to standard design automation tools. The compilation scripts are
+ open and can be safely modified: synthesised circuits are
+ correctbyconstruction. The synthesisable subset of higher order
+ logic can be extended using additional proofbased tools that
+ transform definitions into the subset.",
+ paper = "Gord06.pdf"
+}
+
+\end{chunk}
+
+\index{Guttman, Joshua D.}
+\index{Ramsdell, John D.}
+\index{Wand, Mitchell}
+\begin{chunk}{axiom.bib}
+@article{Gutt95,
+ author = "Guttman, Joshua D. and Ramsdell, John D. and Wand, Mitchell",
+ title = {{VLISP: A Verified Implementation of Scheme}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "8",
+ pages = "532",
+ year = "1995",
+ abstract =
+ "The VL!SP project showed how to produce a comprehensively verified
+ implementation for a programming language, namely Scheme. This paper
+ introduces two more detailed studies on VLISP [13, 21). It summarizes
+ the basic techniques that were used repeatedly throughout the effort.
+ It presents scientific conclusions about the applicability of the
+ these techniques as well as engineering conclusions about the crucial
+ choices that allowed the verification to succeed.",
+ paper = "Gutt95.pdf"
+}
+
+\end{chunk}
+
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@incollection{Hoar72,
+ author = "Hoare, C.A.R",
+ title = {{Notes on Data Structuring}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "83174"
+}
+
+\end{chunk}
+
+\index{Keimel, Klaus}
+\index{Plotkin, Gordon D.}
+\begin{chunk}{axiom.bib}
+@article{Keim09,
+ author = "Keimel, Klaus and Plotkin, Gordon D.",
+ title = {{Predicate Transformers for Extended Probability and
+ NonDeterminism}},
+ journal = "Math. Struct. in Comp. Science",
+ volume = "19",
+ pages = "501539",
+ year = "2009",
+ abstract =
+ "We investigate laws for predicate transformers for the combination of
+ nondeterministic choice and (extended) probabilistic choice, where
+ predicates are taken to be functions to the extended nonnegative
+ reals, or to closed intervals of such reals. These predicate
+ transformers correspond to state transformers, which are functions to
+ conical powerdomains, which are the appropriate powerdomains for the
+ combined forms of nondeterminism. As with standard powerdomains for
+ nondeterministic choice, these come in three flavours – lower, upper
+ and (order)convex – so there are also three kinds of predicate
+ transformers. In order to make the connection, the powerdomains are
+ first characterised in terms of relevant classes of functionals.
+
+ Much of the development is carried out at an abstract level, a kind of
+ domaintheoretic functional analysis: one considers dcones, which are
+ dcpos equipped with a module structure over the nonnegative extended
+ reals, in place of topological vector spaces. Such a development still
+ needs to be carried out for probabilistic choice per se ; it would
+ presumably be necessary to work with a notion of convex space rather
+ than a cone.",
+ paper = "Keim09.pdf"
+}
+
+\end{chunk}
+
+\index{Lamport, Leslie}
+\index{Owicki, Susan}
+\begin{chunk}{axiom.bib}
+@article{Lamp81,
+ author = "Lamport, Leslie and Owicki, Susan",
+ title = {{Program Logics and Program Verification}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "197199",
+ year = "1981",
+ paper = "Lamp81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Manolios, Panagiotis}
+\index{Moore, J Strother}
+\begin{chunk}{axiom.bib}
+@article{Mano03,
+ author = "Manolios, Panagiotis and Moore, J Strother",
+ title = {{Partial Functions in ACL2}},
+ journal = "J. of Automated Reasoning",
+ volume = "31",
+ pages = "107127",
+ year = "2003",
+ abstract =
+ "We describe a method for introducing 'partial functions' into ACL2,
+ that is, functions not defined everywhere. The function 'definitions'
+ are actually admitted via the encapsulation principle: the new
+ function symbol is constrained to satisfy the appropriate
+ equation. This is permitted only when a witness function can be
+ exhibited, establishing that the constraint is satisfiable. Of
+ particular interest is the observation that every tail recursive
+ definition can be witnessed in ACL2. We describe a macro that allows
+ the convenient introduction of arbitrary tail recursive functions, and
+ we discuss how such functions can be used to prove theorems about
+ state machine models without reasoning about “clocks” or counting the
+ number of steps until termination. Our macro for introducing “partial
+ functions” also permits a variety of other recursive schemes, and we
+ briefly illustrate some of them.",
+ paper = "Mano03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Morgan, Carroll}
\begin{chunk}{axiom.bib}
@book{Morg98,
@@ 12544,6 +13152,41 @@ when shown in factored form.
\end{chunk}
+\index{O'Donnell, Michael J.}
+\begin{chunk}{axiom.bib}
+@article{Odon81,
+ author = "O'Donnell, Michael J.",
+ title = {{A Critique of the Foundations of Hoarestyle Programming Logics}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "349374",
+ year = "1981",
+ abstract =
+ "Much recent discussion in computing journals has been devoted to
+ arguments about the feasibility and usefulness of formal
+ verification methods for increasing confidence in computer
+ programs. Too little attention has been given to precise criticism
+ of specific proposed systems for reasoning about programs. Whether
+ such systems are to be used for formal verification, by hand or
+ automatically, or as a rigorous foundation for imformal reasoning,
+ it is essential that they be logically sound. Several popular
+ rules in the Hoare language are in fact not sound. These rules
+ have been accepted because they have not been subjected to
+ sufficiently strong standards of correctness. This paper attempts
+ to clarify the different technical definitions of correctness of a
+ logic, to show that only the strongest of these definitions is
+ acceptable for Hoare logic, and to correct some of the unsound
+ rules which have appeared in the literature. The corrected rules
+ are given merely to show that it is possible to do so. Convenient
+ and elegant rules for reasoning about certain programming
+ constructs will probably require a more flexible notation than
+ Hoare's.",
+ paper = "Odon81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Talpin, JeanPierre}
\index{Jouvelot, Pierre}
\begin{chunk}{axiom.bib}
@@ 12577,6 +13220,31 @@ when shown in factored form.
\end{chunk}
+\index{Leroy, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Lero09,
+ author = "Leroy, Xavier",
+ title = {{A Formally Verified Compiler Backend}},
+ journal = "Logic in Computer Science",
+ volume = "43",
+ number = "4",
+ pages = "363446",
+ year = "2009",
+ abstract =
+ "This article describes the development and formal verification
+ (proof of semantic preservation) of a compiler backend from Cminor
+ (a simple imperative intermediate language) to PowerPC assembly code,
+ using the Coq proof assistant both for programming the compiler and
+ for proving its soundness. Such a verified compiler is useful in the
+ context of formal methods applied to the certification of critical
+ software: the verification of the compiler guarantees that the safety
+ properties proved on the source code hold for the executable compiled
+ code as well.",
+ paper = "Lero09.pdf"
+}
+
+\end{chunk}
+
\section{Proving Axiom Correct  Coercion in CASProof Systesms} %
\index{Sozeau, Matthieu}
@@ 18995,7 +19663,8 @@ when shown in factored form.
must have some personal experience of understanding to attain
belief, and to have this experience you must engage your intuition
and other mental processes which are impossible to formalise.",
 paper = "Poll97.pdf"
+ paper = "Poll97.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 43630,6 +44299,30 @@ ISBN 0897916999 LCCN QA76.95 I59 1995 ACM order number 505950
\end{chunk}
+\index{Lewis, Robert Y.}
+\begin{chunk}{axiom.bib}
+@article{Lewi17,
+ author = "Lewis, Robert Y.",
+ title = {{An Extensible Ad Hoc Interface between Lean and Mathematica}},
+ journal = "EPTCS",
+ volume = "262",
+ pages = "2337",
+ year = "2017",
+ abstract =
+ "We implement a userextensible ad hoc connection between the Lean
+ proof assistant and the computer algebra system Mathematica. By
+ reflecting the syntax of each system in the other and providing a
+ flexible interface for extending translation, our connection allows
+ for the exchange of arbitrary information between the two systems. We
+ show how to make use of the Lean metaprogramming framework to verify
+ certain Mathematica computations, so that the rigor of the proof
+ assistant is not compromised.",
+ paper = "Lewi17.pdf",
+ keywords = "axiomref,printed"
+}
+
+\end{chunk}
+
\index{Liao, HsinChao}
\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
diff git a/changelog b/changelog
index 125427a..4d7c750 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180401 tpd src/axiomwebsite/patches.html 20180401.01.tpd.patch
+20180401 tpd books/bookvolbib add references
20180309 tpd src/axiomwebsite/patches.html 20180309.03.tpd.patch
20180309 tpd books/bookvol13 add chapter Here is the Problem
20180309 tpd src/axiomwebsite/patches.html 20180309.02.tpd.patch
diff git a/patch b/patch
index 5481c88..b4f34a6 100644
 a/patch
+++ b/patch
@@ 1,4 +1,675 @@
books/bookvol13 add chapter Here is the Problem
+books/bookvolbib add references
Goal: Proving Axiom Correct
+\index{Benton, Nick}
+\index{Zarfaty, Uri}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bent07,
+ author = "Benton, Nick and Zarfaty, Uri",
+ title = {{Formalizing and Verifying Semantic Type Soundness of a
+ Simple Compiler}},
+ booktitle = "Principles and Practice of Declarative Programming",
+ publisher = "ACM",
+ pages = "112",
+ year = "2007",
+ abstract =
+ "We describe a semantic type soundness result, formalized in the Coq
+ proof assistant, for a compiler from a simple imperative language with
+ heapallocated data into an idealized assembly language. Types in the
+ highlevel language are interpreted as binary relations, built using
+ both secondorder quantification and a form of separation structure,
+ over stores and code pointers in the lowlevel machine.",
+ paper = "Bent07.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam J.}
+\begin{chunk}{axiom.bib}
+@article{Chli07,
+ author = "Chlipala, Adam J.",
+ title = {{A Certified TypePreserving Compiler from the Lambda Calculus
+ to Assembly Language}},
+ journal = "ACM SIGPLAN PLDI'07",
+ volume = "42",
+ number = "6",
+ year = "2007",
+ pages = "5465",
+ abstract =
+ "We present a certified compiler from the simplytyped lambda calculus
+ to assembly language. The compiler is certified in the sense that it
+ comes with a machinechecked proof of semantics preservation,
+ performed with the Coq proof assistant. The compiler and the terms of
+ its several intermediate languages are given dependent types that
+ guarantee that only welltyped programs are representable. Thus, type
+ preservation for each compiler pass follows without any significant
+ "proofs" of the usual kind. Semantics preservation is proved based on
+ denotational semantics assigned to the intermediate languages. We
+ demonstrate how working with a typepreserving compiler enables
+ typedirected proof search to discharge large parts of our proof
+ obligations automatically.",
+ paper = "Chli07.pdf"
+}
+
+\end{chunk}
+
+\index{Crary, Karl}
+\index{Sarkar, Susmit}
+\begin{chunk}{axiom.bib}
+@misc{Crar08,
+ author = "Crary, Karl and Sarkar, Susmit",
+ title = {{Foundational Certified Code in a Metalogical Framework}},
+ link = "\url{http://repository.cmu.edu/compsci/470/}",
+ year = "2008",
+ abstract =
+ "Foundational certified code systems seek to prove untrusted programs
+ to be safe relative to safety policies given in terms of actual
+ machine architectures, thereby improving the systems' flexibility and
+ extensibility. Using the Twelf metalogical framework, we have
+ constructed a safety policy for the IA32 architecture with a trusted
+ runtime library. The safety policy is based on a formalized
+ operational semantics. We have also developed a complete, foundational
+ proof that a fully expressive typed assembly language satisfies that
+ safety policy",
+ paper = "Crar08.pdf"
+}
+
+\end{chunk}
+
+\index{Fox, Anthony}
+\begin{chunk}{axiom.bib}
+@article{Foxx03,
+ author = "Fox, Anthony",
+ title = {{Formal Specification and Verification of ARM6}}
+ journal = "LNCS",
+ volume = "2758",
+ pages = "2540",
+ year = "2003",
+ abstract =
+ "This paper gives an overview of progress made on the formal
+ specification and verification of the ARM6 microarchitecture using
+ the HOL proof system. The ARM6 is a commercial processor design preva
+ lent in mobile and embedded systems – it features a 3stage pipeline
+ with a multicycle execute stage, six operating modes and a rich
+ 32bit RISC instruction set. This paper describes some of the
+ difficulties encountered when working with a full blown instruction
+ set architecture that has not been designed with verification in mind.",
+ paper = "Foxx03.pdf"
+}
+
+\end{chunk}
+
+\index{Guttman, Joshua D.}
+\index{Ramsdell, John D.}
+\index{Wand, Mitchell}
+\begin{chunk}{axiom.bib}
+@article{Gutt95,
+ author = "Guttman, Joshua D. and Ramsdell, John D. and Wand, Mitchell",
+ title = {{VLISP: A Verified Implementation of Scheme}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "8",
+ pages = "532",
+ year = "1995",
+ abstract =
+ "The VL!SP project showed how to produce a comprehensively verified
+ implementation for a programming language, namely Scheme. This paper
+ introduces two more detailed studies on VLISP [13, 21). It summarizes
+ the basic techniques that were used repeatedly throughout the effort.
+ It presents scientific conclusions about the applicability of the
+ these techniques as well as engineering conclusions about the crucial
+ choices that allowed the verification to succeed.",
+ paper = "Gutt95.pdf"
+}
+
+\end{chunk}
+
+\index{Leroy, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Lero09,
+ author = "Leroy, Xavier",
+ title = {{A Formally Verified Compiler Backend}},
+ journal = "Logic in Computer Science",
+ volume = "43",
+ number = "4",
+ pages = "363446",
+ year = "2009",
+ abstract =
+ "This article describes the development and formal verificat ion
+ (proof of semantic preservation) of a compiler backend from Cminor
+ (a simple imperative intermediate language) to PowerPC assembly code,
+ using the Coq proof assistant both for programming the compiler and
+ for proving its soundness. Such a verified compiler is useful in the
+ context of formal methods applied to the certification of critical
+ software: the verification of the compiler guarantees that the safety
+ properties proved on the source code hold for the executable compiled
+ code as well.",
+ paper = "Lero09.pdf"
+}
+
+\end{chunk}
+
+\index{Dargaye, Zaynah}
+\index{Leroy, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Darg07,
+ author = "Dargaye, Zaynah and Leroy, Xavier",
+ title = {{Mechanized Verification of CPS Transformations}},
+ journal = "LNCS",
+ volume = "4790",
+ pages = "211225",
+ year = "2007",
+ abstract =
+ "Transformation to continuationpassing style (CPS) is often performed
+ by optimizing compilers for functional programming languages. As part
+ of the development and proof of correctness of a compiler for the
+ miniML functional language, we have mechanically verified the
+ correctness of two CPS transformations for a callbyvalue λ
+ $\lambda$calculus with nary functions, recursive functions, data
+ types and patternmatching. The transformations generalize Plotkin’s
+ original callbyvalue transformation and Danvy and Nielsen’s
+ optimized transformation, respectively. We used the Coq proof
+ assistant to formalize the transformations and conduct and check the
+ proofs. Originalities of this work include the use of bigstep
+ operational semantics to avoid difficulties with administrative
+ redexes, and of twosorted de Bruijn indices to avoid difficulties
+ with $\alpha$conversion.",
+ paper = "Darg07.pdf"
+}
+
+\end{chunk}
+
+\index{Manolios, Panagiotis}
+\index{Moore, J Strother}
+\begin{chunk}{axiom.bib}
+@article{Mano03,
+ author = "Manolios, Panagiotis and Moore, J Strother",
+ title = {{Partial Functions in ACL2}},
+ journal = "J. of Automated Reasoning",
+ volume = "31",
+ pages = "107127",
+ year = "2003",
+ abstract =
+ "We describe a method for introducing 'partial functions' into ACL2,
+ that is, functions not defined everywhere. The function 'definitions'
+ are actually admitted via the encapsulation principle: the new
+ function symbol is constrained to satisfy the appropriate
+ equation. This is permitted only when a witness function can be
+ exhibited, establishing that the constraint is satisfiable. Of
+ particular interest is the observation that every tail recursive
+ definition can be witnessed in ACL2. We describe a macro that allows
+ the convenient introduction of arbitrary tail recursive functions, and
+ we discuss how such functions can be used to prove theorems about
+ state machine models without reasoning about “clocks” or counting the
+ number of steps until termination. Our macro for introducing “partial
+ functions” also permits a variety of other recursive schemes, and we
+ briefly illustrate some of them.",
+ paper = "Mano03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Boyer, Robert S.}
+\index{Moore, J Strother}
+\begin{chunk}{axiom.bib}
+@article{Boye75,
+ author = "Boyer, Robert S. and Moore, J Strother",
+ title = {{Proving Theorems About LISP Functions}},
+ journal = "J. ACM",
+ volume = "22",
+ number = "1",
+ pages = "129144",
+ year = "1975",
+ abstract =
+ "Program verification is the idea that properties of programs can be
+ precisely stated and proved in the mathematical sense. In this paper,
+ some simple heuristics combining evaluation and mathematical induction
+ are describe, which the authors have implemented in a program that
+ automatically proves a wide variety of theorems about recursive LISP
+ functions. The method the program uses a generate induction formulas
+ is described at length. The theorems proved by the program include
+ that REVERSE is its own inverse and that a particular SORT program is
+ correct. A list of theorems proved by the program is given.",
+ paper = "Boye75.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.C.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gord89,
+ author = "Gordon, Michael J.C.",
+ title = {{Mechanizing Programming Logics in Higher Order Logic}},
+ booktitle = "Current Trends in Hardware Verification and Automated
+ Theorem Proving",
+ publisher = "Springer",
+ year = "1989",
+ abstract =
+ "Formal reasoning about computer programs can be based directly on the
+ seman tics of the programming language, or done in a special purpose
+ logic like Hoare logic. The advantage of the first approach is that
+ it guarantees that the formal reasoning applies to the language being
+ used (it is well known, for example, that Hoare's assignment axiom
+ fails to hold for most programming languages). The advantage of the
+ second approach is that the proofs can be more direct and natural.
+
+ In this paper, an attempt to get the advantages of both approaches
+ is described. The rules of Hoare logic are mechanically derived
+ from the semantics of a simple imperative programming language
+ (using the HOL system). These rules form the basis for a simple
+ program verifier in which verification conditions are generated by LCF
+ style tactics whose validations use the derived Hoare rules.
+ Because Hoare logic is derived, rather than postulated, it is straight
+ tforw ard to mix seman tic and axiomatic rea soning. It is also
+ forward to combine the constructs of Hoare logic with other
+ applicationspecific notations. This is briefly illustrated for
+ various logical constructs, including termination statements, VDMstyle
+ `relational' correctness specifications, weakest precondition
+ statements and dynamic logic formulae.
+
+ The theory underlying the work presented here is well known. Our
+ contribution is to propose a way of mechanizing this theory in a
+ way that makes certain practical details work out smoothly .",
+ paper = "Gord89.pdf"
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Guessarian, Irene}
+\index{Meseguer, Jose}
+\begin{chunk}{axiom.bib}
+@article{Gues87,
+ author = "Guessarian, Irene and Meseguer, Jose",
+ title = {{On the Axiomatization of 'IfTHENELSE'}},
+ journal = "SIAM J. Comput.",
+ volume = "16",
+ number = "2",
+ year = "1987",
+ abstract =
+ "The equationally complete proof system for "ifthenelse" of Bloom
+ and Tindell (this Journal, 12 (1983), pp. 677707) is extended to a
+ complete proof system for manysorted algebras with extra operations,
+ predicates and equations among those. We give similar completeness
+ results for continuous algebras and program schemes (infinite trees)
+ by the methods of algebraic semantics. These extensions provide a
+ purely equational proof system to prove properties of functional
+ programs over userdefinable data types.",
+ paper = "Gues87.pdf"
+}
+
+\end{chunk}
+
+\index{Keimel, Klaus}
+\index{Plotkin, Gordon D.}
+\begin{chunk}{axiom.bib}
+@article{Keim09,
+ author = "Keimel, Klaus and Plotkin, Gordon D.",
+ title = {{Predicate Transformers for Extended Probability and
+ NonDeterminism}},
+ journal = "Math. Struct. in Comp. Science",
+ volume = "19",
+ pages = "501539",
+ year = "2009",
+ abstract =
+ "We investigate laws for predicate transformers for the combination of
+ nondeterministic choice and (extended) probabilistic choice, where
+ predicates are taken to be functions to the extended nonnegative
+ reals, or to closed intervals of such reals. These predicate
+ transformers correspond to state transformers, which are functions to
+ conical powerdomains, which are the appropriate powerdomains for the
+ combined forms of nondeterminism. As with standard powerdomains for
+ nondeterministic choice, these come in three flavours – lower, upper
+ and (order)convex – so there are also three kinds of predicate
+ transformers. In order to make the connection, the powerdomains are
+ first characterised in terms of relevant classes of functionals.
+
+ Much of the development is carried out at an abstract level, a kind of
+ domaintheoretic functional analysis: one considers dcones, which are
+ dcpos equipped with a module structure over the nonnegative extended
+ reals, in place of topological vector spaces. Such a development still
+ needs to be carried out for probabilistic choice per se ; it would
+ presumably be necessary to work with a notion of convex space rather
+ than a cone.",
+ paper = "Keim09.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation:
+ Introduction}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979"
+ paper = "Gord79.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79a,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: ML}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979"
+ paper = "Gord79a.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur j.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
+@article{Gord79b,
+ author = "Gordon, Michael J. and Milner, Arthur j. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF, A Mechanised Logic of Computation: PPLAMBDA}},
+ journal = "LNCS",
+ volume = "78",
+ year = "1979"
+ paper = "Gord79b.pdf"
+}
+
+\end{chunk}
+
+\index{Lewis, Robert Y.}
+\begin{chunk}{axiom.bib}
+@article{Lewi17,
+ author = "Lewis, Robert Y.",
+ title = {{An Extensible Ad Hoc Interface between Lean and Mathematica}},
+ journal = "EPTCS",
+ volume = "262",
+ pages = "2337",
+ year = "2017",
+ abstract =
+ "We implement a userextensible ad hoc connection between the Lean
+ proof assistant and the computer algebra system Mathematica. By
+ reflecting the syntax of each system in the other and providing a
+ flexible interface for extending translation, our connection allows
+ for the exchange of arbitrary information between the two systems. We
+ show how to make use of the Lean metaprogramming framework to verify
+ certain Mathematica computations, so that the rigor of the proof
+ assistant is not compromised.",
+ paper = "Lewi17.pdf",
+ keywords = "axiomref,printed"
+}
+
+\end{chunk}
+
+\index{Clint, M.}
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@article{Clin72,
+ author = "Clint, M. and Hoare, C.A.R",
+ title = {{Program Proving: Jumps and Functions}},
+ journal = "Acta Informatica",
+ volume = "1",
+ pages = "214224",
+ year = "1972",
+ abstract =
+ "Proof methods adequate for a wide range of computer programs have
+ been expounded in [1] and [2]. This paper develops a method suitable
+ for programs containing functions, and a certain kind of jump. The
+ method is illustrated by the proof of a useful and efficient program
+ for table lookup by logarithmic search.",
+ paper = "Clin72.pdf"
+}
+
+\end{chunk}
+
+\index{Floyd, Robert W.}
+\begin{chunk}{axiom.bib}
+@article{Floy64,
+ author = "Floyd, Robert W.",
+ title = {{Algorithm 245: Treesort}},
+ journal = "CACM",
+ volume = "7",
+ number = "12",
+ year = "1964",
+ pages = "701",
+ paper = "Floy64.pdf"
+}
+
+\end{chunk}
+
+\index{Dijkstra, E.W.}
+\begin{chunk}{axiom.bib}
+@incollection{Dijk72,
+ author = "Dijkstra, E.W.",
+ title = {{Notes on Structured Programming}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "182"
+}
+
+\end{chunk}
+
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@incollection{Hoar72,
+ author = "Hoare, C.A.R",
+ title = {{Notes on Data Structuring}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "83174"
+}
+
+\end{chunk}
+
+\index{Dahl, OleJohan}
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@incollection{Dahl72,
+ author = "Dahl, OleJohan and Hoare, C.A.R",
+ title = {{Hierachical Program Structure}},
+ booktitle = "Structured Programming",
+ publisher = "Academic Press",
+ year = "1972",
+ pages = "175220""
+}
+
+\end{chunk}
+
+\index{Lamport, Leslie}
+\import{Owicki, Susan}
+\begin{chunk}{axiom.bib}
+@article{Lamp81,
+ author = "Lamport, Leslie and Owicki, Susan",
+ title = {{Program Logics and Program Verification}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "197199",
+ year = "1981",
+ paper = "Lamp81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Glasner, Ingrid}
+\index{Loeckx, Jacquest}
+\begin{chunk}{axiom.bib}
+@article{Glas78,
+ author = "Glasner, Ingrid and Loeckx, Jacquest",
+ title = {{A Calculus for Proving Properties of WhilePrograms}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "252281",
+ year = "19"78,
+ paper = "Glas78.pdf",,
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Cartwright, Robert}
+\index{McCarthy, John}
+\begin{chunk}{axiom.bib}
+@article{Cart78,
+ author = "Cartwright, Robert and McCarthy, John",
+ title = {{Recursive Programs as Functions in a First Order Theory}},
+ journal = "LNCS",
+ volume = "75",
+ pages = "576629",
+ year = "1978",
+ abstract =
+ "Pure Lisp style recursive function programs are represented in a new
+ way by sentences and schemata of first order logic. This permits easy
+ and natural proofs of extensional properties of such programs by
+ methods that generalize structural induction. It also systematizes
+ known methods such as recursion induction, subgoal induction,
+ inductive assertions by interpreting them as first order axiom
+ schemata. We discuss the metatheorems justifying the representation
+ and techniques for proving facts about specific programs. We also give
+ a simpler version of the GiSdeIKleene way of representing computable
+ functions by first order sentences.",
+ paper = "Cart78.pdf"
+}
+
+\end{chunk}
+
+\index{Cartwright, Robert}
+\begin{chunk}{axiom.bib}
+@phdthesis{Cart76
+ author = "Cartwright, Robert",
+ title = {{A Practical Formal Semantic Definition and Verification
+ System for Typed LISP}},
+ school = "Stanford Artificial Intelligence Labs",
+ year = "1976",
+ abstract =
+ 'Despite the fact that computer scientists have developed a variety of
+ formal methods for proving computer programs correct, the formal
+ verification of a nontrivial program is still a formidable
+ task. Moreover, the notion of proof is so imprecise in most existing
+ verification systems, that the validity of the proofs generated is
+ open to question. With an aim toward rectifying these problems, the
+ research discussed in this dissertation attempts to accomplish the
+ following objectives:
+ \begin{enumerate}
+ \item To develop a programming language which is sufficiently powerful
+ to express many interesting algorithms clearly and succintly, yet
+ simple enough to have a tractable formal semantic definition
+ \item To completely specify both proof theoretic and model theoretic
+ formal semantics for this language using the simplest possible
+ abstractions
+ \item To develop an interactive program verification system for the
+ language which automatically performs as many of the straightforward
+ steps in a verification as possible
+ \end{enumerate}",
+ paper = "Cart76.pdf",
+}
+
+\end{chunk}
+
+\index{O'Donnell, Michael J.}
+\begin{chunk}{axiom.bib}
+@article{Odon81,
+ author = "O'Donnell, Michael J.",
+ title = {{A Critique of the Foundations of Hoarestyle Programming Logics}},
+ journal = "LNCS",
+ volume = "131",
+ pages = "349374",
+ year = "1981",
+ abstract =
+ "Much recent discussion in computing journals has been devoted to
+ arguments about the feasibility and usefulness of formal
+ verification methods for increasing confidence in computer
+ programs. Too little attention has been given to precise criticism
+ of specific proposed systems for reasoning about programs. Whether
+ such systems are to be used for formal verification, by hand or
+ automatically, or as a rigorous foundation for imformal reasoning,
+ it is essential that they be logically sound. Several popular
+ rules in the Hoare language are in fact not sound. These rules
+ have been accepted because they have not been subjected to
+ sufficiently strong standards of correctness. This paper attempts
+ to clarify the different technical definitions of correctness of a
+ logic, to show that only the strongest of these definitions is
+ acceptable for Hoare logic, and to correct some of the unsound
+ rules which have appeared in the literature. The corrected rules
+ are given merely to show that it is possible to do so. Convenient
+ and elegant rules for reasoning about certain programming
+ constructs will probably require a more flexible notation than
+ Hoare's.",
+ paper = "Odon81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Manna, Zohar}
+\index{Waldinger, Richard}
+\begin{chunk}{axiom.bib}
+@article{Mann78a,
+ author = "Manna, Zohar and Waldinger, Richard",
+ title = {{Is 'sometime' sometimes better than 'always'?}},
+ journal = "CACM",
+ volume = "21",
+ number = "2",
+ year = "1978",
+ abstract =
+ "This paper explores a technique for proving the correctness and
+ termination of programs simultaneously. This approach, the
+ {\sl intermittentassertion method}, involves documenting the
+ program with assertions that must be true at some time when
+ control passes through the corresponding point, but that need not
+ be true every time. The method, introduced by Burstall, promises
+ to provide a valuable complement to the more conventional methods.
+
+ The intermittentassertion method is presented with a number of
+ examples of correctness and termination proofs. Some of these
+ proofs are markedly simpler than their conventional
+ counterparts. On the other hand, it is shown that a proof of
+ correctness or termination by any of the conventional techniques
+ can be rephrased directly as a proof using intermittent
+ assertions. Finally it is shown how the intermittent assertion
+ method can be applied to prove the validity of program
+ transformations and the correctness of continuously operating
+ systems.",
+ paper = "Mann78a.pdf, printed"
+}
+
+\end{chunk}
+
+\index{Katz, Shmuel}
+\index{Manna, Zohar}
+\begin{chunk}{axiom.bib}
+@article{Katz75,
+ author = "Katz, Shmuel and Manna, Zohar",
+ title = {{A Closer Look at Termination}},
+ journal = "Acta Informatica",
+ volume = "5",
+ pages = "333352",
+ year = "1975",
+ abstract =
+ "Several methods for proving that computer programs terminate are
+ presented and illustrated. The methods considered involve (a)
+ using the 'noinfinitelydescendingchain' property of
+ wellfounded sets (Floyd's approach), (b) bounding a counter
+ associated with each loop ({\sl loop} approach), (c) showing that
+ some exit of each loop must be taken ({\sl exit} approach), or (d)
+ inducting on the structure of the data domain (Burstall's
+ approach). We indicate the relative merit of each method for
+ proving termination or nontermination as an integral part of an
+ automatic verification system.",
+ paper = "Katz75.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 3f895eb..4cf5aa5 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5922,6 +5922,8 @@ books/bookvolbib add references
books/bookvolbib add references
20180309.03.tpd.patch
books/bookvol13 add chapter Here is the Problem
+20180401.01.tpd.patch
+books/bookvolbib add references

1.9.1