- "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
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
- "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
- "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
- "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
- "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
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
- "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
- "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
- 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
- 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
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