Algebraic and Logical Methods for the Design 

of Software and Hardware

Staff Members: U Berger, N A Harman, O Kullmann, F G Moller, M Roggenbach, A G Setzer, J V Tucker. 

Honorary Staff: J A Bergstra (Amsterdam), J I Zucker (McMaster), J E Blanck (Lulea), K Stephenson (QinetiQ).

Over the past decade the Department has been involved in first rate research in many areas of the mathematical foundations of computation, including complexity theory, computability theory, concurrency, logic, finite model theory, algebraic specifications, data type theory, rewriting systems, type theory, proof theory and topological computation. Some past members of the group are here.

Swansea theoreticians are among the largest and strongest such groups in the UK with every researcher deeply involved in their personal research programmes and local and international collaborations. There are regular vistors and general and specialist seminars, such as
the Swansea Algebraic Specification Seminar.

Among our subjects of current research are:

Computation on Topological Data Types (J V Tucker)

Topological algebras model continuous data types like the real numbers, waveforms and signals, infinite data streams, state spaces, function spaces, etc.

Our theoretical aim is to create a comprehensive computability theory for functions on topological algebras.

A practical aim is efficient and useful exact methods for specification, computation and reasoning with real numbers.

An applied aim is to use the theory to investigate
    (i) analysis and geometry,
    (ii) analogue and hybrid forms of computation, and
    (iii) physical theory.
Much of this work is in collaboration with J I Zucker (McMaster) and V Stoltenberg-Hansen (Uppsala).

Computability and Physical Systems  (J V Tucker, E J Beggs)

EJB and JVT are developing a theory of functions computable by experiments with physical systems to answer the questions:

What is an experimental procedure and how does it compare with an algorithmic procedure?
Are there useable physical systems that are non-computable?

Examples of exotic low dimensional mechanical systems have been created that can compute all functions but they are not useable. These results lead to an analysis of the construction and observation of physical systems in Gedanken experiments. We are also working on an axiomatic analysis of the information processing of physical systems.

Other theoretical problems are being investigated, for example a recent results
of JVT and J I Zucker (McMaster) have shown: all finite dimensional computably approximable dynamical systems in n-dimensional space are algebraically specifiable.

Algebraic Specification (J V Tucker, M Roggenbach, N A Harman, A. Gimblett)

Algebraic specification methods for software design are a longstanding area of research at Swansea. Currently, MR is active in creating data type libraries, tools and language extensions for the specification language CASL. For example, consistency checkers for specifications and verification tools are being developed, and a concurrent extension called CSP-CASL is being designed and tested. As a major industrial case study, an electronic payment transaction standard is being specified with H Schlingloff (Humbold University and Fraunhofer Institute, Berlin) and the software house Zühlke, Zürich).
An algebraic theory of interfaces has been developed and applied to the analysis of the object-oriented architectures of systems by JVT and K Stephenson. Algebraic specifications of methods are used by NAH in the formal documentation of object-oriented code with tools for animating specifications based on the Maude rewriting system. JVT and MR are working on a theory of libraries of systems.

At Swansea, algebraic methods are also applied in work on topological data types, scientific computation, graphics and hardware.

Models of Computer Systems (N A Harman)

The aim is to create a unified algebraic theory for computers from low-level hardware to high-level programs, using equational methods and tools for specification, simulation, and verification. Algebraic methods for modelling microprocessors at instruction set architecture (ISA) and microarchitecture levels of abstraction, and for proving their equivalence, have been developed and extended to pipelined and superscalar processors. These methods have been adapted for use in HOL verifications at Cambridge, where a complete verification of the ARM 3 architecture has been completed. Algebraic models of object oriented systems at the Application Program Interface level of abstraction are being developed, along with tools to extract executable specifications embedded in C# and Java documentation comments.

Algebraic Methods for Scientific Computation (J V TuckerM Chen)

Synchronous concurrent algorithms (SCAs) are parallel algorithms embedded in a geometrical space and dependent on time. The theory of SCAs provides a unified theory of parallel deterministic systems ranging from models of hardware to models of the heart. At its heart are algebraic specification methods. Recent research has focused on the hierarchical structure of synchronous concurrent algorithms  (SCAs) and the embedding of one SCA into another. The algebraic methods research for the design of topological data types and synchronous concurrent algorithms is also being applied to software for whole heart modelling and simulation. In collaboration with Prof. A V Holden (Biomedical Sciences, Leeds), the hierarchical structure of numerical algorithms was investigated to solve problems in cardiac simulation. Whole heart modelling has also been a case study in the development of constructive volume geometry (CVG), a high-level approach to volume graphics based on algebraic data types by Holden, Chen and Tucker. Other collaborators in this field include Magne Haveraaen (Bergen).

Higher order methods for semantics and program synthesis (U Berger, M Seisenberger)

Higher type semantic models and proof theory have been used for analysing functional languages, and for automatically synthesising provably correct programs. Semantically, the theory of totality in Scott-domains is under investigation. Proof theoretically, the interactive theorem prover MINLOG was developed, and the method of program synthesis from proofs (via realisability interpretations) has been integrated and extended to certain certain nonconstructive logics and logics for polynomial time computability. A fast and very useful program synthesised from a proof is an efficient higher order term rewriting algorithm called normalisation by evaluation.

Dependent Type theory and applications  (A G Setzer)

AGS is working on two main topics. One proof theoretical aim is to determine the limit of formal reasoning (Hilbert's Second Problem), and AGS has determined the strength of various extensions (universes, W-type, reflection principles) of Martin-Löf type theory, including the Mahlo universe and the p3-reflecting universe, the strongest  formal theories currently available in constructive logic. The more practical goal is to apply the expressiveness of dependent types to programming technology, in the areas of generative and of provably correct programming. Together with P. Hancock (Edinburgh), AGS has introduced concepts for representing state-dependent interactive programs in dependent type theory, including a state-dependent monad. Furthermore AGS has, together with P. Dybjer (Gothenburg) developed a data type of inductive-recursive definitions, which allows one to analyse and manipulate data structures -- a very general form of generic programming. AGS is also working on the integration of object technology into dependent type theory.

Infinite State Automata Theory (F G Moller)

Verification tools for modelling systems typically rely on such models being finite state, so as to allow for the complete exploration of state spaces.  The aim of our research is to develop structural techniques which not only extend automated verification to infinite state systems (which, e.g., encode infinite data types), but which also circumvent the state space explosion problem.  Two important tools developed in this study are structural decomposition techniques, and the exploitation of game theoretic interpretations of the various verification problems. Much of this work is done in collaboration with P Jancar (Ostrava) and Y Hirshfeld (Tel Aviv).

Modal and Temporal Logics (F G Moller)

Various program logics have been developed for reasoning about reactive systems, and these have been implemented in a number of tools and used effectively in the verification of practical systems.  The aim of our research is to characterise and interrelate the expressive power of the various logical frameworks, particularly involving fixed point logics. The main tool in this work is the use of Ehrenfeucht-Fraisse games, which characterise the semantic content of these logics.  Much of this work is done in collaboration with A Rabinovich (Tel Aviv).

Satisfiability Problem (O Kullmann)

The satisfiability problems are at the heart of many practical verification techniques. They are also a key to the P=NP Problem. OK has developed general methods for upper bounds on satisfiability problems requiring exponential time, leading to new tools for satisfiability (e.g., specializations and extensions of resolution). The theory of autarkies has been initiated to detect redundancies in propositional formulae. New applications of linear programming, matching theory and matroid theory have been found, unifying and strengthening results on several important classes of propositional formulas with polynomial time satisfiability decision. Recently, with the "combinatorics of conflicts" OK has opened a new area of interactions between combinatorics, graph theory, research on SAT algorithms and algebra. And thorough theoretical and practical investigations into the nature of phase transitions and the interactions of SAT and Statistical Physics have started. OK has the fastest algorithms for satisfiability some of which have been coded in the OK solver and are now public.

Page created by J V Tucker, May 2004.