PUBLICATIONS

• "The relevance of formal verification for system and program design", in Proceedings of the 8th GE Software Engineering Conference, Daytona Beach, FL, (May 1987), (co-author Harry Rosenthal).

Use of a standard system/program design language for specifying designs has a major positive impact on the software life cycle, especially regarding design and code reusability. This paper considers the use of formal verification languages (FVL's), which support proof of design correctness, as system/program design languages. Even when formal verification is not actually performed or required (e.g., to satisfy Department of Defense secure system requirements), it may be efficacious to use an FVL, such as RCA's Verlangen(tm) or GE's Affirm , instead of a standard system/program design language. This paper presents an overview of FVL's and gives some examples to compare their suitability and effectiveness as system/program design languages, cost benefits, etc. Other solutions, including extending Ada and building specialized system/program design languages to meet DoD secure system requirements are also discussed, as is the broader need for design capture tools such as MCC's Leonardo.

• "Verifying with Verlangen", DEC Professional, (Mar. 1987), (co-author: Harry Rosenthal).

Q: Why bother formally verifying systems designs?
A: For critical systems, verified design can increase confidence that a system will meet its requirements. Verifying a system design also can catch flaws early in the product life cycle, while the cost of correcting them is relatively low.

• "Verlangen: formally verifying system designs", RCA Engineer, (Jan./Feb. 1986)

"Verlangen" is a German verb that means "to require." It is also, appropriately, the name of a set of tools for formally specifying system designs and verifying that they meet requirements:

Specification language -- provides high-level languge features for specifying system designs and requirements.

Compiler -- translates a specification into definitions and theorems in first-order logic.

Theorem prover -- proves theorems to verify that a design satisfies requirements.

Verlangen is appropriate for many kinds of computer systems, including distributed systems, communicaitons networks, and operating systems. Eventually, a translator will be added for implementing verified designs in software. Verlangen is being developed by the Software Engineering Laboratory of RCA Advanced Technology Laboratories.

• "Verlangen: a verification language for designs of secure systems", Proceedings of the 8th National Security Conference, Gaithersburg, MD, (Sep.-Oct. 1985).

Verlangen is a language being developed at RCA for formally specifying and verifying system designs. It supports object-oriented design, concurrency, and levels of refinement, and is appropriate for specifying designs of distributed systems, communication networks, and operating systems, and for verifying that the design meet security and other kinds of requirements. A compiler translates a Verlangen text, which is a formal specificaiton of a system design and its requirements, directly into a collection of first-order logic definitions and theorems. Proving the theorems verifies that the design satisfies the requirements. The compiler and theorem prover run under the VAX/VMS operating system.

•  "Verlangen: a verifiable design language for secure systems", Proceedings of AFCEA First Annual Symposium on Physical/Electronic Security, Philadelphia, PA, (August 1985).

Many programing language features are equally valuable for expressing program and design specifications, and are included in Verlangen. These include block structure, identifier scope and visibility rules, user-defined datatypes, and modularity. Nevertheless Verlangen is not a programming language and can be used for specifying systems composed from a combination of hardware and software.

Verlangen encourages system designs and their verifications to be decomposed into tractable units. It accomplishes this through "classes", which support object-oriented design, and "levels", which support levels of refinement (hierarchical design). Verlangen is perhaps unique in its applicability to truly concurrent systems, such as distributed systems and networks, without imposing a restrictive model for communications between subsystems.

• "Formal verification of a secure network with end-to-end encryption", in Proceedings of the 1984 Symposium on Security and Privacy, Oakland, CA, (May 1984).

A formal specification and verification of a simple secure communications network using end-to-end encryption is presented. It is shown that all data sent over the network is encrypted and all hosts on the network exchange messages only if they are authorized to do so. The network and its hosts are modelled by a set of concurrent processes that communicate via unidirectional buffers. Each process is viewed as a state machine. The specification has been formally verified using the commercially-available VERUS verification system.

• "SUPPOSE: A microcomputer operating system for distributed applications", RCA Engineer, (Sep.-Oct. 1981), (co-author. M.E. Stickel).

SUPPOSE, an operating system for dedicated networks of microcomputers, provides a run-time environment for distributed applications as well as a conceptual framework for programming them. SUPPOSE is an acronym for Server Uniform Process Protocol Operating System Environment.

A distributed application running under SUPPOSE consists of a number of cooperating concurrent processes, with one or more processes executing on each microcomputer in the network. SUPPOSE provides facilities for memory, processs, and device management. The services and resources provided and used by an application determine how the application can be decomposed into a set of cooperating processes. Processes may be servers, which provide a service or control a resource, or requestors, which use a service or resource. SUPPOSE supports this conceptual frameworkby providing a set of highly disciplined interprocess communication operations. As a result, SUPPOSE facilitates the design and implementation of distributed applications and makes them comprehensible.

• "An interprocess communication facility for distributed applications", in Proceedings of Fall COMPCON 80, Washington, DC, (Sep. 1980). (co-author M.E. Stickel).

When an application is distributed across several processor nodes, the facilities available for communication and synchronization have a tremendous influence on the ease with which the application program can be designed, written, and understood. This paper presents a framework for structuring a distributed application as a set of concurrent processes and describes a message-based interprocess communication and synchronization facility. This facility, which is supported in a prototype implementation by a kernal-executive called SUPPOSE, is particularly appropriate for loosely-coupled networks where common memory cannot be assumed.

• Incremental Synthesis of Inductive Assertions for Program Verification, Ph.D. Dissertation, The University of Arizona, (Dec. 1977).

An incremental approach to verification is described which permits inductive assertions to be developed step-by-step by finding the individual loop invarianats one at a time and which effectively partitions a program's proof of correctness into a number of smaller, simpler proofs. The approach is called "incremental" because a typical verification consists of several successful passes through a program verifier. The user initiates each pass by augmenting the program with new assertions expressing additional properties of the program. Each successful pass validates these [new] assertions and possibly some additional inductive asssertions as well. Assertions that have been validated in previous passes are recognized in subsequent passes as facts, or lemmas, which can be drawn upon to synthesize and/or validate other assertions. During any one pass, if the inductive assertions supplied with the program are not sufficient to complete the pass, new inductive assertions are generated as they are needed.

• "A Note Concerning Intermittent Assertions, SIGACT News, (Summer 1977). (co-authors R. B. McLaughlin and R. J. Orgass).

In [another article], Manna and Waldinger describe an interesting technique for proving total correctness of programs. Their essential idea is to use loop invariants that, rather than being true for every traversal of the loop, are true only intermittenly. ... The purpose of this note is to illustrate by means of an example the usefulness of intermittent assertions [i.e., invariants] without introducing any new formalism [which would tend to obscure the essentials of the technique].

• Deduce: An Interactive Natural Deduction Theorem Prover, Technical Report, University of Arizona, (May 1977).

Deduce is a program that proves theorems in the first-order predicate calculus with identity using a subordinate proof natural deduction method. In the design of Deduce, emphasis has been placed on achieving natural and intuitive human-machine interaction. This paper describes the interactive facilities of Deduce and, informally, its underlying system of logic.

• Incremental Assertion Synthesis, Technical Report, University of Arizona, (April 1977).

Incremental assertion synthesis is an interactive technique which provides a natural and intuitive way of partitioning a program correctness proof into a number of smaller, simpler proofs. Using the technique, complex inductive assertions, such as those needed for nested loops or to prove complex properties of programs, are constructed incrementally with significantly less effort than would otherwise be required. This paper describes how incremental assertion synthesis works, applies it to several example programs, and releates it to other techniques for assertion synthesis. Also, the organization necessary for a verifier supporting incremental assertion aynthesis is contrasted with the organization of the Stanford Pascal verifier.

• Consistency and Completeness of the Deduction System of Deduce, Technical Report, University of Arizona, (Feb. 1977).

Deduce is an interactive theorem prover, implemented as part of an interactive program verification system. This paper describes D, the natural deduction system of first-order logic used by Deduce. The syntax and rules of inference of D are given, and D is shown to be semantically complete and consistent.

• "Procedure referencing environments in SL5", in Proceedings of the Third ACM Symposium on the Principles of Programming Languages, Atlanta, GA, (Jan. 1976), (co-authors: F.C. Druseikis, R.E. Griswold, D.R. Hanson, and R.A. Holmes).

SL5 is a programming language developed for experimental work in generalized pattern matching and high-level data structuring and access mechanisms. This paper describes the procedure mechanism and the conventions for the interpretation of identifiers in SL5. Procedure invocation in SL5 is decomposed into the separate source-language operations of context creatoin, argument binding and procedure activation, and allows SL5 procedures to be used as recursive functions or coroutines. This decomposition has led to rules for scoping and for the interpretation of identifiers that are different from those found in other programming languages. Several examples of SL5 procedures are given, including a scanner based on the coroutine model of pattern matching.

• Generated Code for PASCAL-10, Technical Report, University of Arizona, (Dec. 1975), (co-author: D.R. Hanson).

This report documents the generated code produced by the PASCAL-10 compiler fo rthe DECsystem-10. This compiler is a modification of the CDC 6400 PASCAL compiler, written in PASCAL. Cross-compilation was used to get PASCAL-10 running. Consequently, the initial (and currently, only) implementation of the PASCAL-10 compiler generates Macro-10 assembly language....

• Heap Storage Management for the Programming Language Pascal, M.S. Thesis, University of Arizona, (Dec. 1975).

The programming language Pascal supports pointer variables, whose objects are typically allocated from a heap, since their allocation and accessibility are only indirectly related to block structure...Automatic storage recovery allows maximum recovery [of program-inaccessible heap objects] without introducing dangling references. ... This thesis shows how heap storage management in Pascal can be designed to allow a hierarchy of implementations. The initial implementation [has] only allocation operations...The second implementation includes non-compacting automatic recovery [and this paper describes] two approaches to determine accessibility: compiler-generated type templates processed by an interpreter, and compiler-generated subroutines. The final implementation adds compaction to the previous one...