Formal Analysis, Theory and Algorithms
The group develops and applies mathematics and logic to the design and analysis of algorithms and complex computational systems. The group is especially interested in bringing the clarity and insight of formal theories to hard application problems of real practical significance. For example, the group has interests in:
- algorithms for matching problems
- combinatorial search and optimization
- computational biology
- constraint programming
- graph algorithms
- modelling and analysis of complex and reactive systems
- phase transition phenomena in combinatorial problems
- probabilistic model checking
- process algebras
- programming language semantics and type systems
- quantum computation
- string algorithms
- telecommunications software and protocol analysis
- theorem proving and deductive reasoning
Many projects are collaborative, as the group aims to apply formal ideas to problems of genuine interest outside the formal community itself. Collaboration involves, for example, life scientists and communication system designers, companies in the telecommunications, software and pharmaceutical sectors, as well as government organisations.
Current:
- A Population Approach to Ubicomp System Design (2011-2016)
- Optimising options and strategies for living donor kidney transplantation for incompatible donor-recipient pairs (2012-2013)
- Kidney Exchange Data Analysis Toolkit (2011)
- VPS: Verifying Interoperability Requirements in Pervasive Systems (2008-2012)
- Homework: Shaping Future User Domestic Infrastructure (2008-2012)
- Stochastic process algebra modelling of ROS regulation in oxidative stress (2007-2011)
- Molecular Nose (2007-2011)
Completed:
- ARTE: Advanced Symmetry Reduction Tools for Explicit State Model Checking
- Software for the National Matching Scheme for Paired Donation
- QNET: Semantics of Quantum Computation
- MATCH UP: Matching Under Preferences - Algorithms and Complexity (2007-2010)
- SIGNAL: Stochastic Process Algebra for Signalling Pathways (2007-2010)
- QICS: QISC: Foundational Structures in Quantum Information and Computation
- Engineering Foundations of Web Services: Theories and Tool Support
- Algorithmics of Stable Matching Problems with Indifference
- Quantum Computation: Foundations, Security, Cryptography and Group Theory
- Behavioural Types for Object-Oriented Languages
- DIAS: Design, Implementation and Adaption of Sensor Networks
- Hybrid Techniques for Detecting and Resolving Feature Interactions in Telecommunications Services (1999-2001)
- Veriscope: Verification of Similar Concurrent Processes (2001-2004)
- Problem Reformulation and Search
- BPS: A Software Tool for the Simulation and Analysis of Biochemical
- FORCES: Forum for the Creation and Engineering of Telecommunications Services
- Dynamic Synthesis of Correct Hardware
- PROSPER: Proof and Specification Assisted Design Environments
- Tree Structures for Algorithmic Problems on Strings
- Stable Matching Algorithms
- User interface design for mechanized theorem proving
- Temporal aspects of verification of LOTOS specifications
- Applications of action semantics
- An Axiomatic Basis for Program Refinement
- Further verification techniques for LOTOS
- Verification techniques for LOTOS
Academic Staff: Prof Muffy Calder, Dr Simon J Gay, Dr Rob Irving, Dr David F Manlove, Dr Alice A Miller, Dr Gethin Norman, Dr Patrick Prosser.
Research Assistants: Dr Oana Andrei, Dr Gregg O'Malley
Research Students: Miss Emma Cummin, Mr Robin Donaldson, Dr Rebecca Mancy, Mr Iain McBride, Mr Iain McGinniss, Mr Ryan Kirwan, Mr Augustine Kwanashie, Mr Yu Lu, Mr Ittoop Puthoor, Mr Michele Sevegnani.
Keywords: theorem proving and model-checking; algorithm design and analysis; design and analysis of software and probabilistic systems; constraint satisfaction; combinatorial optimization; formal methods; feature interaction analysis; concurrency and distributed systems; programming language semantics and type theory; quantum computation; systems biology, bioinformatics and phylogenetics.