Theory
Introduction
The Theory group specialises in the logical, mathematical and statistical foundations of computer science, with a breadth and depth of expertise almost unmatched in the UK. They tackle the hard problems inherent in discovering the power and limitation of computer systems, and how principled design based on the right mathematical models might make them more robust and secure. In addition to achieving various outstanding theoretical results, the group's research has had far-reaching impact, ranging from the way major organisations such as Microsoft, QinetiQ and the CAA think of system verification, to improving the way services are implemented on the World Wide Web.
International quality researchers in this group include Dr Paul Curzon, Dr Hanne Gottliebsen , Dr Kohei Honda, Professor Max Kanovich, Dr Pasquale Malacaria, Professor Ursula Martin, Professor Peter O'Hearn, Dr Paulo Oliva , Dr Soren Riis, Professor Edmund Robinson and Dr Hongseok Yang. Highlights of our research include:
Separation Logic: Professor Peter O'Hearn, Professor Max Kanovich and Dr Hongseok Yang have spearheaded one of the most exciting developments in current Theoretical Computer Science, addressing the 30-year problem of tractable reasoning about data structures held in computer memory. It has led to a powerful new approach to reasoning about shared-memory concurrent programs, methods for combating aliasing in object-oriented programs, and reignited worldwide interest in automatic heap verification, beginning with Dr Hongseok Yang' work. Tool development is under way in collaboration with Microsoft, who are interested in automated validation of their extensive library of device drivers (whose failure is the cause of most Windows system crashes). There is now an active community spanning QM, Microsoft, Imperial, Cambridge, Copenhagen, and Carnegie-Mellon, with teams at Harvard, Stanford, Princeton, Yale, Berkeley, Sydney, Singapore, and Tokyo also building on the work and incorporating it into their tools.
Types for pi-calculus: Dr Kohei Honda's work addresses the foundations of concurrency. He has established a string of results showing the power of types in Milner's classic pi-calculus. In work for the WWW Consortium, he has shown that the same ideas can be used to provide a compact formalism for Web Services Choreography. This now forms an essential part of the W3C's developing approach to the fundamental problem of how to combine and coordinate independent web services to produce powerful and flexible business tools.
Information Theory and Security: Dr Pasquale Malacaria has produced the first successful theoretical foundation for security to combine program theory and Shannon's information theory. Previous program analyses either assume information, like passwords, are secure and cannot be guessed, or that they are completely insecure.
Continuous dynamical systems and computational logic Professor Ursula Martin and Dr Hanne Gottliebsen have developed a novel approach to reasoning about continuous dynamical systems, by bridging mathematical systems theory and Hoare logic. This involves deep theoretical questions requiring a unification of models used in computer science and dynamical systems, as well as practical verification problems spurred by contacts with QinetiQ and Intel. Dr Gottliebsen's interface between the computer algebra system Maple and the theorem prover PVS has been used by others to build industrial tools.
Combinatorics and algorithms: Dr Soren Riis, and Professor Ursula Martin have produced major contributions to long-standing open problems in complexity theory Ursula uses combinatoric techniques in algebra.
Classical Logic: Professor Edmund Robinson has been part of a reinvigoration of classical proof theory where fundamental advances have moved past decades-old stumbling blocks, leading, for the first time, to semantic models that reflect the dynamics of classical sequent calculus. Dr Paulo Oliva' s proof mining work provides a structured way of extracting algorithms from proofs that do not lend themselves readily to this because they use non-constructive principles.
Cognitive Modelling: Dr Paul Curzon has applied techniques from semantics and verification, and used them to construct formal cognitive models, providing a framework that can be used to identify design problems by predicting human error.
Industrial collaboration
Our research whilst theoretical is also practical having a major impact on industrial practice. Highlights of our industrial collaborations include:
Our collaboration with Microsoft on separation logic has resulted in numerous staff exchanges and Microsoft developing an internal separation logic-based analysis tool, SLAyer, which is being successfully applied to Microsoft code and will be rolled out to product divisions within two years.
Professor Ursula Martin has also been involved in industry-funded collaborations with Microsoft to apply formal methods to e-voting. She has also worked with QinetiQ and Intel on formal methods applied to control engineering.
Dr Hanne Gottliebsen has a project with NATS (National Air Transport Services Ltd.) to further develop verification techniques for air traffic control, and a new EU project (MISSA) with Airbus UK, Cert, and Offis on formal methods in aircraft design.
Academic collaboration
Every member of the group is involved in collaboration with other universities in the UK and abroad. Highlights include:
Professor Peter O 'Hearn's seminal work on separation logic was done in collaboration with Reynolds (Carnegie Mellon University, USA)
Dr Kohei Honda's basic work on session-based types for the pi-calculus and its applications was done with Gay (Glasgow), Vasconcelos (Lisbon) and Yoshida (Imperial).
Dr Paul Curzon's work on human error modelling is in collaboration with a UCL team led by Blandford and has led to an international workshop series coordinated with UNU-IIST Macau.
Visit the Theory group webpages.