Computational Logic
1994 Research Review
Summary

William D. Young

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

  1. the CLI stack - a hierarchically-integrated collection of verified components including
  2. the verified Kit kernel,
  3. and many others.
The company distributes and supports the Boyer-Moore Nqthm theorem prover and its interactive enhancement (Pc-Nqthm) and, until recently, maintained the Gypsy Verification Environment.

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.

Acl2

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

  1. J Moore and Matt Kaufmann summarized the key features of the language and of the proof system.
  2. 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.
  3. Larry Akers described his recently completed dissertation research that involves a type information reasoning system for Acl2.
A related presentation was made by Gerard Huet of INRIA (France) on the Coq theorem proving system.

Languages

CLI researchers presented several projects related to defining the semantics of programming languages.

  1. 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.
  2. Mike Smith described an ongoing project to define a semantics for a subset of Ada suitable for analysis.
  3. Larry Akers outlined work aimed at defining a mathematical semantics for a subset of C.
  4. Matt Kaufmann described a technique for extracting verification conditions automatically from annotated programs.

Controllers

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.
  1. 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.
  2. Miren Carranza described the modeling and verification of a fuzzy controller for a simple water tank system.
  3. Bill Young described the modeling of a railroad gate controller using Nqthm.

Systems Software

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.
  1. Bill Bevier described a temporal logic-based model of the Mach operating system kernel.
  2. Larry Smith outlined a plan to use the Mach model as a vehicle for testing particular Mach implementations.
  3. Rich Cohen described the ongoing modeling and proof of a simple separation kernel that provides separated virtual task address spaces on a uniprocessor.
  4. 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.

Hardware

CLI has a very active research program in hardware verification. Hardware related presentations included the following.

  1. 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.
  2. 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.
  3. Ken Albin described validation of Yu's 68020 model by executing the specification and comparing the computed results against an actual 68020 chip.
  4. Larry Smith described a similar validation of CLI's formally verified FM9001 chip description against the fabricated FM9001 chip.
  5. Warren Hunt outlined a joint project with Bob Boyer to code a simulator for the full VHDL hardware description language in Acl2.
  6. 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.

  1. Fay Saydjari of the U.S. Government presented a tool suitable for developing custom netlists for hardware such as DSPs.
  2. Ed Greenwood of Motorola described the design of the DSP under analysis.
  3. Bishop Brock described his efforts in modeling the DSP within Acl2.
  4. 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

This page is URL http://www.computationallogic.com/reviews/94/summary.html