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
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 Tucker, M 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.