Up: Cooperating sites
Previous: Savoie
Sheffield
Fairtlough and Barry Norton are part of the Verification and Testing group in the Department of Computer Science at Sheffield University. This group also includes Graham Birtwistle as Professor Emeritus and has links with Prof. Michael Mendler's Lehrstuhl "Grundlagen der Informatik" at the University of Bamberg (Bamberg subsite).
Fairtlough works with Mendler on a logical approach to computational monads which is known as Lax Logic; this work integrates techniques more commonly used in functional programming with formal verification in Type Theory and in other logical frameworks. The primary application of Lax Logic is to provide a formal framework within which systems can be described and verified over multiple abstraction levels. This work has been recently supported by EPSRC.
Norton has been carrying out research with Mendler within the EPSRC-funded RealType project whose aim was to develop a theory of reactive types for software components used in the development of signal processing applications. His work is in developing techniques which integrate process-algebraic and type theoretic approaches to handling components.
Birtwistle has made major contributions to the formal verification of hardware using both process algebra and higher-order logic and continues to work in this area.
The group will contribute to the following objective:
- Correctness of computer systems: to work on real-time systems and the associated approaches to logical reasoning.
The senior people involved are
- Matt Fairtlough, contact person
- Graham Birtwistle
- Barry Norton
Bengt Nordström 2005-09-22