William D. Young
1994 Research Review
Computational Logic, Inc. (CLI) specializes in advanced research
and development in mathematical modeling of digital hardware and
software systems. (Mathematical modeling in CLI parlance
encompasses what is commonly referred to by the less precise term
formal methods. CLI regards formal methods as ambiguous and
not adequately suggestive of its principle research activity, the
application of rigorous mathematical reasoning to achieve reliable
digital systems.) Notable examples of CLI's research include
The company distributes and supports the
Boyer-Moore Nqthm theorem prover and its interactive
enhancement (Pc-Nqthm) and, until recently, maintained the Gypsy Verification
- the CLI stack - a hierarchically-integrated collection of
verified components including
- a compiler for a simple high-level language (Micro-Gypsy),
- assembler and linker for the Piton assembly-level language, and
- the FM9001 microprocessor
- the verified Kit kernel,
- and many others.
CLI bi-annually hosts a public review to showcase its research
and to obtain feedback from professional colleagues and sponsors. The
1994 review was held April 20--22 in Austin. Approximately 60
representatives of academia, industry, and government attended the
CLI presented research on a variety of topics in automated reasoning
and software and hardware verification. Although presentations were
diverse, one consistent theme was evident. Earlier CLI tools and
techniques for modeling and analyzing digital systems tended to be
applied to small, special-purpose systems designed with formal
analysis in mind and often ignoring many hard real-world issues
considered difficult from a formal modeling perspective. Current CLI
research is aimed at demonstrating the feasibility of applying these
tools and techniques to more realistic applications, including
languages, hardware modules, and system software of genuine commercial
interest (Ada, C, VHDL, Mach, DSPs).
In the remainder of this note we very briefly summarize the content of
the research review. Additional information about any of the topics
presented or a CLI publication list can be obtained from CLI (contact
firstname.lastname@example.org). Further details are available under Mosaic by looking at
the slides pointed to by the 1994 Research Review agenda.
Acl2 is the proposed successor to the Boyer-Moore
Nqthm theorem prover. It is currently under development by Bob Boyer,
Matt Kaufmann, and J Moore at CLI and is expected to provide the
foundation for future CLI modeling and analysis research. The logic
of Acl2 is an applicative subset of Common Lisp consistent with
commercial implementations. The logic is supported by a powerful
A related presentation was made by Gerard Huet of INRIA (France) on
the Coq theorem proving system.
- J Moore and Matt Kaufmann summarized the key features of the
language and of the proof system.
- John Cowles (a CLI consultant) from the University of Wyoming
described the development of libraries of definitions and lemmas
to support arithmetic reasoning with Acl2.
- Larry Akers described his recently completed dissertation
research that involves a type information reasoning system for Acl2.
CLI researchers presented several projects
related to defining the semantics of programming languages.
- Art Flatau described his recently completed dissertation
research on a formally verified compiler from the Boyer-Moore
Nqthm logic to the Piton assembly level language. This project
included the specification of dynamic storage allocation and
- Mike Smith described an ongoing project to define a
semantics for a subset of Ada suitable for analysis.
- Larry Akers outlined work aimed at defining a mathematical semantics
for a subset of C.
- Matt Kaufmann described a technique for extracting verification
conditions automatically from annotated programs.
One of the developing application areas of
CLI's mathematical modeling technology is control and associated
real-time issues. Several presentations were related to this topic.
- Matt Wilding gave back-to-back presentations on: mechanically
supported proof of a classic scheduling algorithms, and the modeling and
verification of real-time applications written for a version of the
- Miren Carranza described the modeling and verification of a
fuzzy controller for a simple water tank system.
- Bill Young described the modeling of a railroad gate controller
A strong research thread within CLI
has been verification of system software, such as the
CLI stack and Bill Bevier's verification of an operating system kernel
(Kit). Current research that builds on that foundation was presented.
- Bill Bevier described a temporal logic-based model of the Mach
operating system kernel.
- Larry Smith outlined a plan to use the Mach model as a vehicle
for testing particular Mach implementations.
- Rich Cohen described the ongoing modeling and proof of a simple
separation kernel that provides separated virtual task
address spaces on a uniprocessor.
- Bill Bevier described the development of a theory of
noninterference-style security and the use of this theory in analyzing
several simple trusted computing bases.
CLI has a very active research program in
hardware verification. Hardware related presentations included the
- Warren Hunt described an approach to extending CLI's research
into modeling and verifying hardware to encompass analysis of digital
signal processors (DSPs). Hunt and Ed Greenwood of Motorola outlined
an ongoing project to model a Motorola DSP.
- Yuan Yu, formerly a student of Bob Boyer at UT and currently
at DEC, described his surprisingly painless adaptation of his
dissertation work modeling the Motorola 68020 user instruction set
to handle the DEC Alpha processor.
- Ken Albin described validation of Yu's 68020 model by executing
the specification and comparing the computed results against an actual
- Larry Smith described a similar validation of CLI's formally
verified FM9001 chip description against the fabricated FM9001 chip.
- Warren Hunt outlined a joint project with Bob Boyer to code a
simulator for the full VHDL hardware description language in Acl2.
- David Russinoff described the definition of a
semantics for a subset of VHDL intended to support mechanical proof.
DSP Design Session
The third day of the research
seminar was a proprietary session devoted to the CLI/Motorola
collaboration aimed at modeling and verifying portions of a Motorola
commercial DSP. In addition to Warren Hunt's introduction to the
project, there were presentations on the following topics.
- Fay Saydjari of the U.S. Government presented a tool suitable for
developing custom netlists for hardware such as DSPs.
- Ed Greenwood of Motorola described the design of the DSP under
- Bishop Brock described his efforts in modeling the DSP within
- Ken Albin and Warren Hunt described the modeling and formal
verification of the implementation of two algorithms on the DSP: a
reciprocal algorithm and a fast fourier transform.
This page is URL http://www.computationallogic.com/reviews/94/summary.html