Theses & Reports

Instructions for submitting a technical report or thesis.

You can find technical reports published prior to 1990 archived here.

Title

Authors

Year

Ph.D. Thesis 1980 The Transformational Approach to the Development and Verification of Programs in a very High Level Language Deak, Edith Gail Abstract | PDF

Title: The Transformational Approach to the Development and Verification of Programs in a very High Level Language

Candidate: Deak, Edith Gail

Abstract:

In informal exposition, the correctness of a complex algorithm is often demonstrated by deriving it through successive refinement steps from a high level specification, and supplying proofs of the underlying principles used in the process. However, most existing mechanical program verifiers ignore this standard expository practice, and are generally designed to verify programs written in a low level form. While logically simple algorithms can be handled adequately in this manner, attempting to verify more complex algorithms at a low level requires treatment of implementation details which obscure the main arguments of the verification. This thesis describes a systematic technique for proving algorithms correct using a transformational approach, and presents a detailed transformation/verification scenario of the proof of a variety of complex combinatorial algorithms. The algorithms treated here are considerably more involved than those verified by other methods. The programming language used is a variant of SETL, adapted for program verification, which provides a medium for high level specification. A program P is annotated with logical formulae of set theory, which are called assumptions and assertions. P is said to by partially correct if every computation which satisfies all assumptions also satisfies all assertions. In order to prove the correctness of P, which initially contains only assumptions, we apply proof rules which are used both to transform the program into logical formulae called verification conditions and then to prove these verification conditions. The transformation rules are unique in that they enable the combination of correct program fragments. We are able to reuse general code fragments in a variety of contexts without reproof and to derive several different low level algorithms from a single high level algorithm. The transformations often require proof of enabling conditions. In such cases, when a transformation is performed, the enabling condition is introduced into the program text as an assumption which must be verified in turn using the proof mechanism described above.
Ph.D. Thesis 1980 An Implementation for Gyve: a Language for Concurrent Processing Meyer, Jeanine Marietta Abstract | PDF

Title: An Implementation for Gyve: a Language for Concurrent Processing

Candidate: Meyer, Jeanine Marietta

Abstract:

This thesis presents a design for implementing a programming language, called GYVE, for specifying groups of concurrent processes such as operating systems. GYVE was designed by Philip Shaw and is described in his dissertation (New York University, 1978). Important features of GYVE include compile time protection checking, explicit scheduling of processes and a dynamic destroy function. The present work contains a detailed review of most of the constructs of GYVE and discussion of how various features could be modified so as to ease the implementation and/or increase performance in certain situations. One such feature concerns accessing of shared objects. This thesis specifies the syntactic and semantic phases of a GYVE compiler and the runtime structures and procedures required for execution of output from the compiler. Included with the specification is a reconcilation of the definition of GYVE implicit in the implementation with the formal definition of Shaw. Shaw gives his formal definition of the compilation process in the form of a two-level grammar. This is compared with the BNF-based syntactic and semantic phases of the implementation. Shaw's runtime system is specified through procedures written in GYVE. The specification code of the implementation is in a low level form of SETL in which we refer to various system tables of fixed sizes, machines with finite storage, semaphores and a simple timer mechanism. An analysis is given of the use of semaphores as required by the existence of the destroy function and the desire to prevent deadlock.
Ph.D. Thesis 1980 Optimization of Inductive Assertions Warren, Jr., Henry Stanley Abstract | PDF

Title: Optimization of Inductive Assertions

Candidate: Warren, Jr., Henry Stanley

Abstract:

Inductive assertions are assertions placed in the loops of a program, primarily for the purpose of aiding a mechanical correctness prover to prove that the program is correct. Here we assume that the assertions in a program are executed along with the program. That is, the predicate expression of each assertion is evaluated when encountered during program execution, to verify that its value is true. Inductive assertions are particularly expensive in terms of execution time. This is not only because they are in loops, but also because they are frequently themselves loops (quantified expressions). Thus executing them can slow a program's execution by a factor that can be indefinitely large. For example, executing them can change an O(n('2)) process to an O(n('3)) process. This thesis investigates the possibility of optimizing such quantified inductive assertions by substantially reducing the range of quantification. It is shown that many inductive assertions encountered in practice fall into a simple pattern in which the quantifier may, essentially, be removed. This restores the execution time of the program to the same order of magnitude that it would have been if the inductive assertions were not executed. Emphasis is placed on methods that are no more costly in compiler size and execution time than conventional global optimization techniques.