Prof.Dr. Egon Boerger

Dipartimento di Informatica, Universita di Pisa

The Evolving Algebra Approach to Specification and Verification of Complex Computer Systems.

DIMACS Center - Room 431
Busch Campus
Piscataway, New Jersey
October 6, 1995 at 10:30 AM


The huge gap between much of academic theory and the prevailing software and hardware practice is still with us, as is a wide-spread scepticism about the industrial benefit of formal methods. In this talk I will present a new general method for software and hardware design which is based upon Gurevich's notion of evolving algebra and contributes to bridging this gap. I will explain that it offers a mathematically well founded and rigorous but nevertheless simple discipline practical and scalable to industrial applications.

I will present the salient features of this new method and illustrate them through several examples from my work on specification and verification of programming languages, compilers, protocols and architectures. The definition of a mathematical model for Hennessy and Patterson's RISC architecture DLX serves as a running example for which we can prove the correctness of instruction pipelining. I will point out the yet unexplored potential of the evolving algebra method for large-scale industrial applications.

This talk serves as survey to direct the attention of the audience to the more specific and technical work which I am willing to present in further talks during my stay at DIMACs.