COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	@Entry(Code "STAN-CS-81-870",
C00008 ENDMK
C⊗;
@Entry(Code "STAN-CS-81-870",
	Title "Optimal Pagination Techniques for Automatic Typesetting Systems",
	Author "Michael F. Plass",
	Price "$4.30", not available,
	Note "77 pages",
	Date "June 1981")

@Entry(Code "STAN-CS-81-871",
	Title "Good Layouts for Patern Recognizers",
	Author "Howard W. Trickey",
	Price "$2.45", not available,
	Note "15 pages",
	Date "August 1981")




@Entry(Code "STAN-CS-81-872",
	Title "Synthesis of Communicating Processes from Temporal Logic 
	      Specifications",
	Author "Zohar Manna and Pierre Wolper",
	Price "$2.85", FREE,
	Note "28 pages",
	Date "September 1981")

In this  paper,  we  apply  Propositional  Temporal  Logic  (PTL)  to  the
specification and synthesis of  the synchronization part of  communicating
processes.  To specify a process, we give a PTL formula that describes its
sequence of communications. The synthesis is done by constructing a  model
of the given specifications using a tableau-like satisfiability  algorithm
for PTL. This model can then be interpreted as a program.

@Entry(Code "STAN-CS-81-873",
	Title "Virtual Memory Management",
	Author "Richard William Carr",
	Price "$8.90", FREE,
	Note "230 pages",
	Date "August 1981")




@Entry(Code "STAN-CS-81-874",
	Title "Multiprocessing Architectures for Local Computer Networks",
	Author "Alfred Z. Spector",
	Price "$5.75", FREE,
	Note "125 pages",
	Date "August 1981")




@Entry(Code "STAN-CS-81-875",
	Title "Computation of Matrix Chain Products, Part I, Part II",
	Author "T. C. Hu and M. T. Shing",
	Price "$5.70", FREE,
	Note "124 pages",
	Date "September 1981")

This paper considers the computation of matrix chain products of the  form
(M[1] x M[2] x...x M[n-1]). If  the matrices are of different  dimensions,
the order  in which  the matrices  are multiplied  affects the  number  of
operations. An optimum order is an  order that minimizes the total  number
of operations.  We  present  some  theorems  about  an  optimum  order  of
multiplying the matrices. Based on these theorems, an O(n log n) algorithm
for finding an optimum order is presented.

@Entry(Code "STAN-CS-81-877",
	Title "Verification of Sequential Programs:  Temporal Axiomatization",
	Author "Zohar Manna",
	Price "$3.35", FREE,
	Note "45 pages",
	Date "September 1981")

This is one in a series of reports describing the application of temporal
logic to the specification and verification of computer programs.
 
In earlier reports, we introduced temporal logic as a tool for reasoning
about concurrent programs and specifying their properties
and presented proof principles for establishing these properties.
Here, we restrict ourselves to deterministic, sequential programs.  
We present a proof system in which properties of such programs, 
expressed as temporal formulas, can be proved formally.

Our proof system consists of three parts:  a  general part elaborating 
the properties of temporal logic, a domain part giving an axiomatic 
description of the data domain, and a  program part giving an axiomatic
description of the program under consideration.

We illustrate the use of the proof system by giving two alternative 
formal proofs of the total correctness of a simple program.