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