1994 Research Review

Summary

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 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 review.

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 elster@cli.com). Further details are available under Mosaic by looking at the slides pointed to by the 1994 Research Review agenda.

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

- 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 garbage collection.
- 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.

- 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 CLI stack.
- 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 using Nqthm.

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

- 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 68020 chip.
- 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.

- 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 analysis.
- Bishop Brock described his efforts in modeling the DSP within Acl2.
- 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.

http://dirleton.csres.utexas.edu/reviews/94/summary.html