Papers

Computer Arithmetic: Logic, Calculation and Rewriting

by M.Benini, D.Nowotka and C.Pulley. Frontiers of Combining Systems (FroCoS'98), October 2nd-4th 1998, University of Amsterdam

Abstract

This paper describes the concepts behind the Computer Arithmetic Toolkit (CAT) for the Isabelle/HOL system written by the authors.

Full paper: [PDF]

Workshop

Holly: An Approach to Object Code Verification

by M. Benini, S. Kalvala, D. Nowotka and C. Pulley. 5th Annual Automated Reasoning Workshop (ARW 5) Bridging the Gap between Theory and Practice co-located with the 14th BCTCS, St. Andrews, 1998.

Abstract

Formal verification of software typically consists in checking programs in a high-level language against an abstract specification. Confidence on the correctness of the actual program running on a machine also relies on the soundness of the translation from the high-level language to the machine code, i.e., the correctness of a compiler, including its code optimisation techniques.

If one wishes to have confidence on the final code, another approach is object code verification, i.e., verification of program code at assembly level. Now the confidence in the implementation of a program on an actual machine is more direct, relying on the correctness of the hardware model and no other software.

But, dealing with object code also has a price. It is, in a sense, further away from its specification because it has to deal with a more concrete machine, considering registers, limited memory, and so on. There is a vast shift in granularity between code and specification.

The technique for object code verification we are developing emphasises the use of abstraction, aided by a process algebraic framework. The concept of simulation provides the tool with which abstractions on the process algebraic representation of the program can be formalised.

However, the correctness proof takes place in higher-order logic (HOL), which we believe presents a more amenable proof environment. Abstraction at the logical level is obtained by unlifting results from the CCS level using the CCS semantics. More precisely, let < be a simulation relation, and let [| - |]^s be the lifting operator for a particular sequence s of states, then:

If P < Q then ∀ s · [| P |]^s ⇒ [| Q |]^s .
The interaction between the logical and the algebraic level is fundamental for our methodology.

We have implemented this approach in a proof system we call Holly. We use Isabelle/HOL, in which we embedded a variation of Milner's Calculus of Communicating Systems (CCS) as a process algebra. When verifying a program, its object code is translated both into a representation in HOL and an equivalent representation in CCS. At any point in a proof either deductions in HOL or simulations in the process algebra can be used.

Holly demonstrates the concurrent use of a logical and an algebraic model to make object code verification feasible. In this talk, we expand on the interaction between these models, and highlight the interaction within an example proof in Holly.

Code Releases

CAT is a Computer Arithmetic Toolkit for the Isabelle/HOL theorem prover. It provides a theory for integers, a rewrite engine for integer expressions, and a decision procedure for Presburger formulas.

Version 1.0 beta of CAT is available here which requires Isabelle94-8 and Poly ML 3.2.

  • Source code distribution: CAT.tgz
  • Documentation (also included in the distribution):