The Evolving Algebra Methodology for Design and Analysis of Complex SW/HW Systems

The lectures introduce the main features of the evolving algebra approach to mathematical specification and verification of complex real-life SW and HW systems. The methodology is based upon Gurevich's notion of evolving algebra. It provides the possibility of rigourous abstract analysis of non-trivial behaviour of large systems and nevertheless presupposes only general abilities and experience in programming. We illustrate the notion through a correctness proof for a general pipelining scheme on RISC architectures.