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:

Completed:

  • 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.

Real-time verification of wireless home networks using bigraphs with sharing
Calder, M. , Koliousis, A. , Sevegnani, M. , and Sventek, J. (2013) Real-time verification of wireless home networks using bigraphs with sharing. Science of Computer Programming . ISSN 0167-6423 (doi:10.1016/j.scico.2013.08.004 ) (In Press)

The joy of matching
Harrenstein, P., Manlove, D. , and Wooldridge, M. (2013) The joy of matching. IEEE Intelligent Systems , 28 (2). pp. 81-85. ISSN 1541-1672 (doi:10.1109/MIS.2013.49 )

Equivalence checking of quantum protocols
Ardeshir-Larijani, E., Gay, S. , and Nagarajan, R. (2013) Equivalence checking of quantum protocols. In: Piterman, N. and Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 19th International Conference, TACAS 2013, Rome, Italy,16-24 March 2013. Series: Lecture notes in computer science, 7795 . Springer Heidelberg, Dordrecht, The Netherlands, pp. 478-492. ISBN 9783642367410

Quantum process calculus for linear optical quantum computing
Franke-Arnold, S. , Gay, S.J. , and Puthoor, I. (2013) Quantum process calculus for linear optical quantum computing. In: Dueck, G.W. and Miller, M. (eds.) Reversible Computation: Proceedings of the 5th International Conference, RC 2013, Victoria, BC, Canada, 4-5 July 2013. Series: Lecture notes in computer science, 7948 . Springer Heidelberg, Dordrecht, The Netherlands, pp. 234-246. ISBN 9783642389856

Techniques for formal modelling and analysis of quantum systems
Gay, S.J. , and Nagarajan, R. (2013) Techniques for formal modelling and analysis of quantum systems. In: Coecke, B. and Ong, L. (eds.) Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky: Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. Series: Lecture notes in computer science, 7860 . Springer Heidelberg, Dordrecht, The Netherlands, pp. 264-276. ISBN 9783642381638

Socially stable matchings in the hospitals / residents problem
Askalidis, G., Immorlica, N., Kwanashie, A., Manlove, D.F. , and Pountourakis, E. (2013) Socially stable matchings in the hospitals / residents problem. Lecture Notes in Computer Science , 8037 . pp. 85-96. ISSN 0302-9743 (doi:10.1007/978-3-642-40104-6_8 )

Mitochondrial reactive oxygen species enhance AMP-activated protein kinase activation in the endothelium of patients with coronary artery disease and diabetes
MacKenzie, R.M. et al. (2013) Mitochondrial reactive oxygen species enhance AMP-activated protein kinase activation in the endothelium of patients with coronary artery disease and diabetes. Clinical Science , 124 (6). pp. 403-411. ISSN 0143-5221 (doi:10.1042/CS20120239 )

Stable matching problems with exchange restrictions
Irving, R.W. (2008) Stable matching problems with exchange restrictions. Journal of Combinatorial Optimization , 16 (4). pp. 344-360. ISSN 1382-6905 (doi:10.1007/s10878-008-9153-1 )

Sex-equal stable matchings: complexity and exact algorithms
McDermid, E. , and Irving, R.W. (2013) Sex-equal stable matchings: complexity and exact algorithms. Algorithmica . ISSN 0178-4617 (doi:10.1007/s00453-012-9672-0 ) (In Press)

Optimal stable marriage
Irving, R.W. (2008) Optimal stable marriage. Working Paper. Springer US.

Algorithmics Of Matching Under Preferences
Manlove, D. (2013) Algorithmics Of Matching Under Preferences. Series: Theoretical Computer Science . World Scientific Publishing. ISBN 9789814425247

Guest editorial: special issue on matching under preferences
Manlove, D. , Irving, R. , and Iwama, K. (2010) Guest editorial: special issue on matching under preferences. Algorithmica , 58 (1). pp. 1-4. ISSN 0178-4617 (doi:10.1007/s00453-010-9415-z )

A constraint model and a reduction operator for the minimising open stacks problem
Miller, A. , Prosser, P. , and Unsworth, C. (2005) A constraint model and a reduction operator for the minimising open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews, St. Andrews, UK, pp. 44-50.

Improved lower bounds for solving the minimal open stacks problem
Miller, A. (2005) Improved lower bounds for solving the minimal open stacks problem. In: Constraint Modelling Challenge 2005, in Conjunction with The Fifth Workshop on Modelling and Solving Problems with Constraints Held at IJCAI 2005, Edinburgh, Scotland, 31 Jul 2005. School of Computer Science, University of St. Andrews, St. Andrews, UK, pp. 36-43.

The use of an electronic voting system in a formal methods course
Miller, A. , and Cutts, Q. (2006) The use of an electronic voting system in a formal methods course. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University, Hamilton, ON, Canada, pp. 3-8.

Evaluating a formal methods technique via student assessed exercises
Donaldson, A.F., and Miller, A. (2006) Evaluating a formal methods technique via student assessed exercises. In: Boute, R.T. and Oliveira, J.N. (eds.) Formal Methods in the Teaching Lab: Examples, Cases, Assignments and Projects Enhancing Formal Methods Education. A Workshop at the Formal Methods 2006 Symposium, Hamilton, Ontario, Canada, 26 Aug 2006. McMaster University, Hamilton, ON, Canada, pp. 93-98.

Formal proof of abstraction for agent-based learning systems
Kirwan, R., and Miller, A. (2013) Formal proof of abstraction for agent-based learning systems. In: 20th Workshop on Automated Reasoning ARW 2013, 11-12 Apr 2013, Dundee, UK.

Solving the rehearsal problem with planning and with model checking
Gregory, P., Miller, A. , and Prosser, P. (2004) Solving the rehearsal problem with planning and with model checking. In: Workshop on Modelling and Solving Problems with Constraints, 22 Aug 2004, Valencia, Spain.

An application of abstraction and induction techniques to degenerating systems of processes
Miller, A. , and Calder, M. (2003) An application of abstraction and induction techniques to degenerating systems of processes. In: International Workshop on Model-Checking for Dependable Software-Intensive Systems, 22-25 Jun 2003, San Francisco, CA, USA.

Timed analysis of RFID distance bounding protocols
Lu, Y., and Miller, A. (2012) Timed analysis of RFID distance bounding protocols. In: Schmidt, R.A. and Papacchini, F. (eds.) Proceedings of the 19th Workshop on Automated Reasoning ARW 2012, Manchester, UK, 2-4 Apr 2012. School of Computer Science, The University of Manchester, Manchester, UK, pp. 37-38.

This Week’s EventsAll Upcoming EventsPast Events

This Week’s Events

There are no events scheduled for this week

Upcoming Events

There are no upcoming events scheduled.

Past Events

Of bison and bigraphs: modelling interactions in physical/virtual spaces (15 May, 2012)

Speaker: Muffy Calder

Mixed reality systems present a wide range of challenges for formal modelling -- how can we model interactions in both physical and virtual spaces? We start to explore this question through a specific application: modelling Steve Benford's Savannah game using Bigraphical reactive systems. The Savannah game is a collaborative, location-based game in which groups of `lions' (i.e. children with devices) hunt together on a virtual savannah that is overlaid on a (physical) open playing field. This work is in the preliminary stages and so unusually for a formal methods talk, we will not give the details of *any* formal models! Instead we will focus on which aspects of the game we can formalise and reason about, and assumptions about the level of detail required for the physical space and for the virtual space.

Empirical Computer Science: how not to do it (09 October, 2012)

Speaker: Patrick Prosser

Empirical Computer Science is hard. To do it well you have to be ruthlessly honest and more than a little bit paranoid. I will present two examples of "How Not to do Empirical Computer Science". NOTE: "All persons, places, and events in this presentation are real. Certain speeches and thoughts are necessarily constructions by the presenter. No names have been changed to protect the innocent, since God Almighty protects the innocent as a matter of Heavenly routine." (quote plagiarized from Kurt Vonnegut's The Sirens of Titan)

Pi-Cost and a brief introduction to DR-PI-OMEGA and DR-PI - Towards Formalizing the Cost of Computation in a Distributed Computer Network (16 October, 2012)

Speaker: Manish Gaur

The picalculus is a basic abstract language for describing communicating processes and has a very developed behavioural theory expressed as equivalence relation between process descriptors; A process P equivalent to a process Q signifies that although P and Q may be intentionally very different they offer essentially same behaviour to the users. The basic language and its related theory has been extended in myriad ways in order to incorporate many different aspect of concurrent behaviour. In this talk, we present a new variation on the picalculus, picost, in which the use of channels must be paid for. Processes operate relative to a cost environment; and communication can only happen if principals have provided sufficient funds for the channels associated with the communications. We define a bisimulation based behavioural preorder in which processes are related if, intuitively, they exhibit the same behaviour but one may be efficient than the other. We justify our choice of preorder by proving that it is characterised by three intuitive properties which behavioural preorders should satisfy in a framework in which the use of resources must be funded.

This development, apart from other applications, is useful in formalising a distributed network with routers acting as an active component in determining the quality of service of the network. We developed two formal languages for distributed networks where computations are described explicitly in the presence of routers. Our model may be considered as an extension of the asynchronous distributed pi-calculus (ADpi). We believe that such models help in prototyping the routing algorithms in context of large networks and reasoning about them while abstracting away the excessive details. Being general, the model may also be applied to demonstrate the role of routers in determining the quality of services of the network. Further in this talk, we intend to very briefly describe the frame work and results obtained about such descriptions.

An Integer Programming Approach to the Hospitals/Residents Problem with Ties (06 November, 2012)

Speaker: Augustine Kwanashie

Matching problems generally involve the assignment of agents of one set to those of another. Often some or all of the agents have preferences over one another. An example of such a problem is the Hospitals/Residents problem with Ties (HRT) which models the problem of assigning graduating medical students to hospitals based on agents having preferences over one another, which can involve ties. Finding a maximum stable matching given an HRT instance is known to be NP-hard. We investigate integer programming techniques for producing optimal stable matchings that perform reasonably well in practice.  Gains made in the size of these matchings can deliver considerable benefits in some real-life applications. We describe various techniques used to improve the performance of these integer programs and present some empirical results.

The Trials and Tribulations of Typestate Inference (13 November, 2012)

Speaker: Iain McGinniss

Typestate is the combination of traditional object-oriented type theory with finite state machines that represent allowable sequences of method calls. A textual definition of a typestate, as required in specifying the type of a function parameter, is verbose to the point of being impractical. Therefore it is desirable to be able to omit such definitions where they can be accurately inferred. In this talk, I shall discuss my attempts to formally define and prove a typestate inference algorithm for a simple calculus, TS1.

PEPA and the Diffusion Problem (20 November, 2012)

Speaker: Michael Jamieson

PEPA, a formalism for keeping track of events during interacting stochastic processes, has been advocated in this School for use in biological investigations. An example is the study of nitric oxide diffusing in a blood vessel. In this talk I will suggest that PEPA be regarded as complementary to another method, which I will describe, of accounting for this diffusion.

A model checking approach for air traffic control requirement analysis (04 December, 2012)

Speaker: Michele Sevegnani

NATS provides air traffic navigation services to over 6,000 aircraft flying through UK controlled airspace every day. The huge challenge faced by the engineering team at the NATS control centre in Prestwick is to monitor constantly the status of the equipment required to provide safe and efficient en route services. This involves interpreting and unstructured data feed generated by thousands of diverse sensors such as communication link monitors but also intrusion sensors.
In this talk we will describe how stochastic modelling and checking can be employed to help in this task. Our models allow us to quantify the overall performance of the monitoring system and the quality of the service provided, to predict future behaviours, to react to external events and to plan future upgrades by identifying weaknesses of the system and optimise assets.

The Hospitals Residents Problem with Couples (11 December, 2012)

Speaker: Iain McBride

The Hospitals Residents Problem (HR) is a familiar problem which seeks a stable bipartite matching amongst two sets: one containing residents and one containing hospitals. Each group expresses a strict linear preference over some subset of the members of the other set. The problem is well understood and an efficient algorithm due to Gale and Shapley exists which guarantees to find a stable matching in an instance of HR.

However, the problem becomes intractable when the residents are able to form linked pairs, or couples. This problem is known as the Hospitals Residents Problem with Couples (HRC). In this case Ronn has previously shown that the problem of deciding whether a stable matching exists in an instance of HRC is NP-complete. We show that this NP-completeness result holds for very restricted versions of HRC. Further, we provide an IP formulation for finding a stable matching in an instance of HRC, or reporting that the instance supports no stable matching, and provide early empirical results derived from this IP model.

On Al Roth Nobel Prize-winning lecture (29 January, 2013)

Speaker: David Manlove

The 2012 Sveriges Riksbank Prize in Economic Sciences in Memory of Alfred Nobel (commonly known as the Nobel Prize in Economics) was awarded jointly to Professors Alvin E Roth and Lloyd S Shapley (see http://www.nobelprize.org/nobel_prizes/economics/laureates/2012/) "for the theory of stable allocations and the practice of market design".

Lloyd Shapley is the co-author of the famous Gale-Shapley algorithm (with David Gale, who sadly died in 2008).  Al Roth has been instrumental in turning theory into practice through his involvement with centralised clearinghouses in many application domains, including junior doctor allocation and kidney exchange, in addition to contributing many important theoretical results himself.

The Nobel Prize announcement was made on 15 October, and the two laureates gave their award lectures on 8 December before receiving the awards on 10 December.  We will watch Al Roth’s lecture, entitled “The Theory and Practice of Market Design” (43 mins).  This is highly relevant to FATA research, as well as being very accessible to anyone who is interested in knowing “who gets what” when it comes to sharing around scarce resources.

Model Checking Port-Based Network Access Control for Wireless Networks (26 February, 2013)

Speaker: Yu Lu

With the rapid development of Internet, the security of network protocols becomes the focus of research. The 802.1X standard is the IEEE standard for port-based network access control. The 802.1X standard delivers powerful authentication and data privacy as part of its robust, extensible security framework. It is this strong security, assured authentication, and dependable data protection that has made the 802.1X standard the core ingredient in today’s most successful network access control (NAC) solutions. As the central access authentication, the importance of IEEE 802.1X protocol's security properties is obvious. Formal methods is an crucial software and protocol analysis and verification tool. Formal methods includes model checking, logic inference, and theorem proving, etc.

We could use model checking to help analyse security protocols by exhaustively inspecting reachable composite system states in a finite state machine representation of the system. The IEEE 802.1X standard provides port-based network access control for hybrid networking technologies. We describe how the current IEEE 802.1X mechanism for 802.11 wireless networks can be modelled in the PROMELA modelling language and verified using the SPIN model checker. We aim to verify a set of essential security properties of the 802.1X, and also to find out whether the current combination of the IEEE 802.1X and 802.11 standards provide a sufficient level of security.

Formal Models for Populations of User Activity Patterns and Varieties of Software Structures (05 March, 2013)

Speaker: Oana Andrei

The challenges raised by developing mobile applications come from the way these apps interweave with everyday life and are distributed globally via application centres or stores to a wide range of users. People use an app according to their needs and understanding, therefore one could observe variations in usage frequencies of features or time and duration of use. The same mobile app varies with app settings, mobile device settings, device model or operating system.

For this talk we present work in progress on a formal modelling approach suitable for representing and analysing the user activity patterns and the structural variability of a software system. It is based on a stochastic abstraction of the populations of software in use and the software uses, building upon results from statistical analysis of user activity patterns. One aim of our current research is to design for variability of uses and contexts that mobile software developers may not be able to fully predict. Based on the automatically logged feedback on in-app usage and configurations, inference methods and formal modelling and analysis connect and collaborate to provide information on relevant populations of similar user behaviour and software structure and to evaluate their performance and robustness. This way we can track behavioural changes in the population of users and suggest software improvements to fit new user behaviours and contexts and changes in the user behaviour. The software designers and developers will then (re)consider the design objectives and strategies, create more personalised modules to be incorporated in the software and identify new opportunities to improve the overall user experience. We use a real life case study based on an iOS game to illustrate the concepts.

This talk is based on a joint work with Muffy Calder, Mark Girolami and Matthew Higgs.

Extremal graphs (12 March, 2013)

Speaker: Patrick Prosser and Alice Miller

Using formal stochastic models to guide decision making -- Should I fix this problem now or in 3 hours? (19 March, 2013)

Speaker: Michele Sevegnani

NATS is the UK's main air navigation service provider. Its control centre in Prestwick constantly monitors the status of its infrastructure via thousands of sensors situated in numerous radar and communication sites all over the UK's territory. The size and complexity of this system often makes it difficult to interpret the sensed data and impossible to predict the system's future behaviour.

In this talk, we present on-going work in which a stochastic model is used to guide decision making. In particular, we will show a prototype web-app based on the formal model that could allow the engineering team in the control room to perform stochastic model checking in a simple and intuitive way, without prior knowledge of formal methods. The analysis results can then be used to schedule, prioritise and optimise maintenance, without affecting safety.

A hierarchy related to interval orders (16 April, 2013)

Speaker: Sergey Kitaev

A partially ordered set (poset) is an interval order if it is isomorphic to some set of intervals on the real line ordered by left-to-right precedence. Interval orders are important in mathematics, computer science, engineering and the social sciences. For example, complex manufacturing processes are often broken into a series of tasks, each with a specified starting and ending time. Some of the tasks are not time-overlapping, so at the completion of the first task, all resources associated with that task can be used for the following task. On the other hand, if two tasks have overlapping time periods, they compete for resources and thus can be viewed as conflicting tasks.

A poset is said to be (2+2)-free if no two disjoint 2-element chains have comparable elements. In 1970, Fishburn proved that (2+2)-free posets are precisely interval orders. Recently, Bousquet-Mélou, Claesson, Dukes, and Kitaev introduced ascent sequences, which not only allowed us to enumerate interval orders, but also to connect them to other combinatorial objects, namely to Stoimenow's matchings, to certain upper triangular matrices, and to certain pattern avoiding permutations (a very active area of research these days). A host of papers by various authors has followed this initial paper.

In this talk, I will review some of results from these papers and will discuss a hierarchy of objects related to interval orders.

The Hospitals/Residents problem with Free pairs (30 April, 2013)

Speaker: Augustine Kwanashie

In the classical Hospitals/Residents problem, a blocking pair exists with respect to a matching if both agents would be better off by coming together, rather than remaining with their partners in the matching (if any). However blocking pairs that exist in theory need not undermine a matching in practice. The absence of social ties between agents may cause a lack of awareness about the existence of blocking pairs in practice. We define the Hospitals/Residents problem with Free pairs (HRF) in which a subset of acceptable resident-hospital pairs are identified as free. This means that they can belong to a matching M but they can never block M. Free pairs essentially correspond to resident and hospitals that do not know one another. Relative to a relaxed stability definition for HRF, called local stability, we show that locally stable matchings can have different sizes and the problem of finding a maximum locally stable matching is NP-hard, though approximable within 3/2. Furthermore we give polynomial time algorithms for two special cases of the problem.  This is joint work with David Manlove.

 

On List Colouring and List Homomorphism of Permutation and Interval Graphs (28 May, 2013)

Speaker: Jessica Enright

List colouring is an NP-complete decision problem even if the total number of colours is three. It is hard even on planar bipartite graphs. I give a sketch of a polynomial-time algorithm for solving list colouring of permutation graphs with a bounded total number of colours. This generalises to a polynomial-time algorithm that solves the list-homomorphism problem to any fixed target graph for a large class of input graphs including all permutation and interval graphs.

On being the CSA for Scottish Government (04 June, 2013)

Speaker: Muffy Calder

An overview of what I do in "the other job".