🚀 go-pugleaf

A Technical Report (details below) containing references to papers of
historical interest in the area of `formal methods' is available
either by FTP from

            m1.cs.man.ac.uk (130.88.13.4)

	    pub/TR/umcs-92-12-2.ps.Z

or in hard copy by e-mailing

            jenny@cs.man.ac.uk

+++++++++++++++++++++++++++++++++++++++++++++++++++++++

Formal Methods -- Selected Historical References

C. B. Jones and A. M. McCauley
	Department of Computer Science
	University of Manchester
	Oxford Rd., Manchester, U.K.

\date{1992-12-09}

Abstract

This report contains citations to papers which are of
historical interest in the area of formal approaches
to software development. 

+++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++

Also available in hard copy (no ftp for copyright reasons) is

+++++++++++++++++++++++++++++++++++++++++++++++++++++++
The Search for Tractable Ways of Reasoning about Programs

C.\ B.\ Jones

\date{1992-03-31 (minor typographical errors corrected: 1992-06-23)}

Abstract

This paper traces the most important steps in the history of research
on reasoning about programs.
The main focus is on ways of verifying that sequential imperative
programs satisfy their specifications.
Over time it has become clear that {\em post facto} verification is
only practical for small programs;
verification methods which support the development of larger programs
exploit a notation of compositionality.
Coping with concurrent algorithms is much more challenging --
this and other extensions are considered briefly.
The main thesis is that the idea of reasoning about programs has been
around for a long time;
the search has been to find tractable methods.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++