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.

This Week’s EventsAll Upcoming EventsPast Events

This Week’s Events

FATA Seminar - Choreographies in the wild

Formal Analysis, Theory and Algorithms
Speaker: Massimo Bartoletti
Date: 25 November, 2014
Time: 16:00 - 17:00
Location: Sir Alwyn Williams Building, 423 Seminar Room

Distributed applications can be constructed by composing services which interact by exchanging messages according to some global communication pattern, called choreography. Under the assumption that each service adheres to its role in the choreography, the overall application is
communication-correct.

However, in wild scenarios like the Web or cloud environments, services may be deployed by different participants, which may be mutually distrusting (and possibly malicious). In these cases, one can not assume (nor enforce) that services always adhere to their roles.

Many formal techniques focus on verifying the adherence between services and choreographic roles, under the assumption that no participant is malicious; in this case, strong communication-correctness results can be obtained, e.g. that the application is deadlock-free. However, in wild
scenarios such techniques can not be applied.

In this talk we present a paradigm for designing distributed applications in wild scenarios. Services use contracts to advertise their intended communication behaviour, and interact via sessions once a contractual agreement has been found. In this setting, the goal of a designer is to realise honest services, which respect their contracts in all execution contexts (also in those where other participants are malicious).

A key issue is that the honesty property is undecidable in general. In this talk we discuss verification techniques for honesty, targeted at agents specified in the contract-oriented calculus CO2. In particular, we show how to safely over-approximate the honesty property by a model-checking technique which abstracts from the contexts a service may be engaged with.

Upcoming Events

FATA Seminar - Choreographies in the wild

Formal Analysis, Theory and Algorithms
Speaker: Massimo Bartoletti
Date: 25 November, 2014
Time: 16:00 - 17:00
Location: Sir Alwyn Williams Building, 423 Seminar Room

Distributed applications can be constructed by composing services which interact by exchanging messages according to some global communication pattern, called choreography. Under the assumption that each service adheres to its role in the choreography, the overall application is
communication-correct.

However, in wild scenarios like the Web or cloud environments, services may be deployed by different participants, which may be mutually distrusting (and possibly malicious). In these cases, one can not assume (nor enforce) that services always adhere to their roles.

Many formal techniques focus on verifying the adherence between services and choreographic roles, under the assumption that no participant is malicious; in this case, strong communication-correctness results can be obtained, e.g. that the application is deadlock-free. However, in wild
scenarios such techniques can not be applied.

In this talk we present a paradigm for designing distributed applications in wild scenarios. Services use contracts to advertise their intended communication behaviour, and interact via sessions once a contractual agreement has been found. In this setting, the goal of a designer is to realise honest services, which respect their contracts in all execution contexts (also in those where other participants are malicious).

A key issue is that the honesty property is undecidable in general. In this talk we discuss verification techniques for honesty, targeted at agents specified in the contract-oriented calculus CO2. In particular, we show how to safely over-approximate the honesty property by a model-checking technique which abstracts from the contexts a service may be engaged with.

FATA Seminar - Russian Dolls Search

Formal Analysis, Theory and Algorithms
Speaker: Ciaran McCreesh
Date: 02 December, 2014
Time: 16:00 - 17:00
Location: Sir Alwyn Williams Building, 423 Seminar Room

Russian Doll Search is a general algorithmic technique for solving hard optimisation problems, which looks a bit like Branch and Bound combined with Dynamic Programming. I'll give an overview of how it works, and what it's been used for, and will then speculate about how we might parallelise it.

FATA Seminar - TBA

Formal Analysis, Theory and Algorithms
Speaker: Roland Perera
Date: 09 December, 2014
Time: 16:00 - 17:00
Location: Sir Alwyn Williams Building, 423 Seminar Room

FATA Seminar - Quiz / Open problems session

Formal Analysis, Theory and Algorithms
Speaker:
Date: 16 December, 2014
Time: 16:00 - 17:00
Location: Sir Alwyn Williams Building, 422 Seminar Room

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

FATA Seminar (22 October, 2013)

Speaker: Various

FATA Seminar (29 October, 2013)

Speaker: Patrick Prosser

In the stable roommates problem we have n agents, where each agent ranks all other agents. The problem is then to match agents into pairs such that no two agents prefer each other to their matched partners. A remarkably simple constraint encoding is presented that uses O(n^2) binary constraints, and in which arc-consistency (the phase-1 table) is established in O(n^3) time. This leads us to a specialised n-ary constraint that uses O(n) additional space and establishes arc-consistency in O(n^2) time. An empirical study is presented and it is observed that the n-ary constraint model can read in, model and output all matchings for an instances with n = 1,000 in about 2 seconds on current hardware platforms. This leads us to a question: egalitarian SR is NP-hard, but where are the hard problems?

FATA Seminar (05 November, 2013)

Speaker: Muffy Calder

A short talk outlining the definition and role of new probabilistic meta models of user activity  patterns for a mass deployed app - how can reasoning about the meta models include future developments of an app? A lively fusion of formal modelling, model checking, HCI and statistics, courtesy of the Populations project.

FATA Seminar (12 November, 2013)

Speaker: Dimitrios Kouzapas

This paper proposes a new bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence.

FATA Seminar - Cliques, Bicliques, Clubs and Colours (19 November, 2013)

Speaker: Ciaran McCreesh

A clique in a graph is a set of vertices, each of which is adjacent to every other vertex in this set. Finding a maximum clique is one of the fundamental NP-hard problems. We discuss how a branch and bound algorithm using greedy graph colouring can be used to solve this problem in practice. We then show how to adapt the algorithm to find maximum independent sets, maximum balanced bicliques, and maximum k-cliques (if a clique is a set of friends, a 2-clique is a set of people who are either friends or who have a mutual friend, and a k-clique is a set of people separated by distance at most k). We finish with a discussion about k-clubs, which are a stricter variation of k-cliques.

FATA Seminar - Two-sided Matching with Partial Information (26 November, 2013)

Speaker: Baharak Rastegari

"Two-sided matching markets model many practical settings, such as corporate hiring and university admission. In the traditional model, it is assumed that all agents have complete knowledge of their own preferences. As markets grow large, however, it becomes impractical for agents to precisely assess their rankings over all agents on the other side of the market. We propose a novel model of two-sided matching in which agents start with partial information about their preferences, but are able to refine this information via interviews. Our goal is to design a centralized interview policy that guarantees the outcome to be stable and optimal for one side of the market, while minimizing the number of interviews. We give evidence suggesting that the problem is hard in the general case, and show that it is polynomial-time solvable in a restricted, yet realistic, setting."

FATA Seminar - What do we mean by persistence in stochastic models? (10 December, 2013)

Speaker: Rebecca Mancy

 
In this talk I will present some of the research I'm currently working on relating to disease persistence in structured populations (e.g. those that have spatial structure or multiple host species). I will briefly introduce the model that prompted this work and the analytic theory associated with it that gives a measure of persistence capacity and a persistence threshold for deterministic models. I will then describe the computational study that I am currently working on to establish the extent to which this threshold is informative about behaviour in a stochastic version of the model.
 
In the second part of the talk, I will introduce several definitions of persistence from the literature and others that I have briefly considered, explaining why I believe that these don't fully capture what it is that we want to know about the system. Finally, I will introduce (early thoughts on) a new measure of stochastic persistence that I am working on, highlighting aspects of implementation that might provide interesting problems in algorithm development.
 

FATA Seminar - Christmas Quiz (17 December, 2013)

Speaker: Simon Gay

2 months in California: from bigraphs to autonomous vehicles (+ a bit of sunshine) (21 January, 2014)

Speaker: Michele Sevegnani

Professor Sengupta's group at UC Berkeley has been investigating the use of the BigActor Model as a formalism for modelling and controlling systems of autonomous vehicles such as Unmanned Air Vehicles (UAV) Autonomous Surface Vehicles (ASV) and Autonomous Underwater Vehicles (AUV). BigActors are distributed concurrent computational entities that interact with a dynamical structure of the world modelled as a bigraph. An example application of BigActors is the specification of environmental monitoring missions in which teams of autonomous vehicles collaborate for locating and tracking oil spills in the ocean.
The aim of my recent visit to UC Berkeley was to adapt and combine the modelling and verification approach developed at Glasgow for the the Homework run-time verification system with the BigActor Model in order to define a general framework for analysis of mobile robotic systems.
In this talk, I will present the first step in this direction: an encoding of BigActors to bigraphs. This is work in progress.

Session Types Revisited (28 January, 2014)

Speaker: Ornela Dardha

Session types are a formalism to model structured communication- based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to the syntax of standard π-calculus types and terms, they give rise to ad- ditional separate syntactic categories. As a consequence, when new type features are added, there is duplication of efforts in the theory: the proofs of properties must be checked both on ordinary types and on session types. We show that session types are encodable in ordinary π types, relying on linear and variant types. Besides being an expressivity result, the encoding (i) removes the above redun- dancies in the syntax, and (ii) the properties of session types are derived as straightforward corollaries, exploiting the correspond- ing properties of ordinary π types. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism and higher-order communications.

FATA Seminar - Stability in networks (04 February, 2014)

Speaker: Ágnes Cseh

The well-known notion of stable matchings can be extended in several interesting ways, one of them operates with network flows. The stable flow problem lies on the border of Mathematics, Economics and Computer Science. We are given a directed network, where the vertices symbolize vendors, while the edges stand for the possible deals between them. We talk about stability if there is no pair of vendors who mutually want to change the current flow of goods. In this talk, we shorty summarize the results currently known about the problem. Besides showing algorithms to find such flows, we also sketch problems related to max flows, flows over time, restricted edges, multicommodity flows and uncoordinated markets.

FATA Seminar - An Exact Branch and Bound Algorithm with Symmetry Breaking for the Maximum Balanced Induced Biclique Problem (11 February, 2014)

Speaker: Ciaran McCreesh

Garey and Johnson's Hard Problem GT24 is to determine whether a given graph contains a balanced induced biclique of a particular size. We already have some good algorithms for the maximum clique problem---we adapt these, to introduce the first branch and bound algorithm for the maximum balanced induced biclique problem.

But why care about balanced induced bicliques? We are not aware of any applications (although other biclique variants do show up in data mining). Instead, we are interested because the problem has some nice properties from an algorithmic perspective: solutions are reasonably well-behaved, and it has the simplest possible non-trivial symmetry. We show how the the symmetry can be removed, using only two small lines of code. But how much easier does this make the problem? How do symmetries interact with branch and bound? What about parallel branch and bound? And what's going on with random graphs?

FATA Seminar - Sudoku as an Assessed Exercise in Constraint Programming: an analysis of student programming ability (18 February, 2014)

Speaker: Patrick Prosser

In the Constraint Programming course (Masters) the first exercise is to code up a solver for the Sudoku puzzle, investigating the effect of using 2 subtly different models and checking that problem instances do indeed have unique solutions. I will present snippets of java code from the 29 students who submitted work. Much of this presentation will be entertaining, but the underlying message is rather serious.

FATA Seminar - Backbones for equality (25 February, 2014)

Speaker: Mike Codish

Mike is visiting the school between 24th and 26th February, 2014. His research interests include the development and application of formal techniques to aid in the compilation and implementation of sequential and concurrent logic programs and to analyse, optimise and reason about such programs.  In this talk Mike will give a general introduction to his work. Specifically, he will describe his structured approach to solving finite domain constraint problems through an encoding to SAT, and the BEE tool (Ben-Gurion Equi-propogation Encoder). He will introduce the notion of the backbone of a CNF formula, and describe his recent work, in which backbones are generalized to capture equations between literals.

FATA Seminar - Verification of Concurrent Quantum Protocols by Equivalence Checking (04 March, 2014)

Speaker: Simon Gay

We present a tool which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. In general, simulation of quantum systems using current computing technology is infeasible. We restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms.

In particular, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of the concurrent system.
Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity.  This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states.

Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using this approach, we have applied our equivalence checking tool to specify and verify interesting and practical quantum protocols from teleportation to secret sharing.

Joint work with Ebrahim Ardeshir-Larijani and Rajagopal Nagarajan.

FATA Seminar - Verifying Differential Privacy by Program Logic (11 March, 2014)

Speaker: Marco Gaboardi

Differential Privacy is becoming a standard approach in data privacy: it offers ways to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Many specific queries have been shown to be differentially private, but manually checking that a given query is differentially private can be both tedious and rather subtle. Moreover, this process becomes unfeasible when large programs are considered.

In this talk I will introduce the basics of differential privacy and some of the fundamental mechanisms for building differentially private programs. Additionally, I will present a verification approach based on Hoare Logic useful to certify a broad range of probabilistic programs as differentially private.

FATA Seminar - Profile-based optimal matchings in the Student/Project Allocation (18 March, 2014)

Speaker: Augustine Kwanashie

In the Student/Project Allocation problem (SPA) we seek to assign students
to group or individual projects offered by lecturers. Students are required
to provide a list of projects they find acceptable in order of preference.
Each student can be assigned to at most one project and there are
constraints on the maximum number of students that can be assigned to each
project and lecturer.  A matching in this context is a set of
student-project pairs that satisfies these constraints.
We seek to find matchings that satisfy optimality criteria based on the
profile of a matching. This is a vector whose ith component indicates the
number of students obtaining their ith-choice project. Various profile-based
optimality criteria have been studied. For example, one matching M1 may be
preferred to another matching M2 if M1 has more students with first-choice
projects than M2.
In this talk we present an efficient algorithm for finding optimal matchings
to SPA problems based on various well known profile-based optimality
criteria. We model SPA as a network flow problem and describe a modified
augmenting path algorithm for finding a maximum flow which can then be
transformed to an optimal SPA matching. This approach allows for additional
constraints, such as project and lecturer lower quotas, to be handled
flexibly without modifying the original algorithm.

Canonical Labelling of Graphs (29 April, 2014)

Speaker: Dr Alice Miller

Many of us in FATA are concerned with symmetry in combinatorial objects, specifically in the use of isomorphism checking to eliminate copies of the same object during their generation, or to prevent redundant work during combinatorial search (for example, during model checking). I have been using the graph isomorphism package, nauty, for years, and eventually decided that I should find out how it works!

The most efficient method used for graph isomorphism checking is that of using a certificate, or cononical labelling . A canonical labelling is a function C that maps any graph to a natural number in such a way that C(G1)=C(G2) if and only if G1 and G2 are isomorphic. In this talk I discuss canonical labelling of trees, and of graphs in general. For the latter, I describe the popular algorithm using equitable partitions used by the most successful graph isomorphism programs such as nauty. The talk will include explanatory examples and  pictures and no pseudocode!

Do I need to fix a failed component now, or can I wait until tomorrow? (06 May, 2014)

Speaker: Prof Muffy Calder

Ideally in systems in which failures are monitored and sensed, an engineer would fix a failure immediately. But this might not be possible due to limited resources and/or physical distance to a device. So how does an engineer prioritise and make best use of their resources, while still ensuring the service is operating within acceptable levels of risk of failure?

We hypothesise predictive event-based modelling and reasoning with a stochastic temporal logic can inform decision making when failures occur. We show, with a real industrial case study (a safety critical comms system for NATS), that by relating the status of assets to service behaviour in a CTMC model, the risk of service failure now, and over various time frames, future failure rates, and interventions, can be quantified. We reason both in the context of how the system is designed to meet service requirements, and how it actually meets service requirements, when the models are calibrated with rates derived from historical, field data.

Mining Behavior Models from User-Intensive Web Applications (06 May, 2014)

Speaker: Dr Giordano Tamburrelli

Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions.
In this talk we present a preliminary approach called BEAR that automates the acquisition of user-interaction requirements in an incremental and reflective way. More precisely, the approach builds upon inferring a set of probabilistic Markov models of the users’ navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. BEAR builds on top of a well established formal tool, indeed it analyzes the inferred models to verify quantitative properties by means of probabilistic model checking. The talk discusses the capabilities of BEAR and illustrates the preliminary results obtained on a Web application currently in use.

Mining Behavior Models from User-Intensive Web Applications (13 May, 2014)

Speaker: Dr. Giordano Tamburrelli

Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions.
In this talk we present a preliminary approach called BEAR that automates the acquisition of user-interaction requirements in an incremental and reflective way. More precisely, the approach builds upon inferring a set of probabilistic Markov models of the users’ navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. BEAR builds on top of a well established formal tool, indeed it analyzes the inferred models to verify quantitative properties by means of probabilistic model checking. The talk discusses the capabilities of BEAR and illustrates the preliminary results obtained on a Web application currently in use.

Reasoning about Optimal Stable Matchings under Partial Information (20 May, 2014)

Speaker: Baharak Rastegari

We study two-sided matching markets in which participants are initially endowed with partial preference orderings, lacking precise information about their true, strictly ordered list of preferences. We wish to reason about matchings that are stable with respect to agents' true preferences, and which are furthermore optimal for one given side of the market. We present three main results. First, one can decide in polynomial time whether there exists a  matching that is stable and optimal under all strict preference orders that refine the given partial orders, and can construct this matching in polynomial time if it does exist. We show, however, that deciding whether a given pair of agents are matched in all or no such optimal stable matchings is co-NP-complete, even under quite severe restrictions on preferences. Finally, we describe a polynomial-time algorithm that decides, given a matching that is stable under the partial preference orderings, whether that matching is stable and optimal for one side of the market under some refinement of the partial orders.

Complex networks and complex processes (27 May, 2014)

Speaker: Professor Simon Dobson

There is increasing interest in using complex networks to model phenomena, and especially in the construction of systems of networks that interact and respond to each other -- the so-called complex adaptive coupled networks. They seem to offer a level of abstraction that is appropriate for capturing the large-scale dynamics of real-world processes without becoming lost in the detail. This talk introduces such networks for a formal audience, describes some recent work in urban traffic modelling, and speculates on the combination of complex networks with sensor data to study environmental incidents such as flooding.

FATA Summer Summary, or, how did you spend your summer? (07 October, 2014)

Speaker: FATA members

FATA Seminar - An introduction to knot theory (14 October, 2014)

Speaker: Brendan Owens

I will give a gentle introduction to mathematical knot theory, focusing on combinatorial aspects that may be of interest to computing scientists, and avoiding technical details.  Topics include knot diagrams and Reidemeister moves, knots and graphs, tabulation of knots, and some discussion of ways of encoding knots.  I will include a brief description of my ongoing search for alternating ribbon knots (joint with Frank Swenton).

FATA Seminar - New Software Applications for Kidney Exchange (21 October, 2014)

Speaker: David Manlove

In this talk I will give some background to kidney exchange in the UK context, and present some recent results from quarterly matching runs.  I will then give an overview of two new software applications for kidney exchange that emerged from summer MSc projects.  The first of these, due to Tommy Muggleton, is a tool for visualising input datasets and optimal solutions for kidney exchange problem instances.  The second, due to James Trimble, allows datasets to be generated that are a better reflection of the UK real data than a previous generator produced, and also permits characteristics of datasets to be analysed, and optimal solutions to be compared and contrasted with respect to different optimality criteria.

FATA Seminar - Size versus truthfulness in the House Allocation problem (28 October, 2014)

Speaker: Baharak Rastegari

I will present our result from last year (presented in EC 2014) on designing truthful mechanisms for the House Allocation (HA) problem. HA is the problem of allocating a set of objects among a set of agents, where each agent has ordinal preferences (possibly involving ties) over a subset of the objects. We focus on truthful mechanisms without monetary transfers for finding large Pareto optimal matchings.  

FATA Seminar - Linear numeral systems (04 November, 2014)

Speaker: Ian Mackie

We take a fresh look at an old problem of representing natural numbers in the lambda-calculus.  Our interest is in finding representations where we can compute efficiently (and where possible, in constant time) the following functions: successor, predecessor, addition, subtraction and test for zero. Surprisingly, we find a solution in the linear lambda-calculus, where copying and erasing are not permitted.

FATA Seminar - Subgraph Isomorphism Problem: simple algorithms (11 November, 2014)

Speaker: Patrick Prosser

In the subgraph isomorphism problem (SIP), we are given two graphs, G and H where G is a the pattern graph and H the target. The problem is then to determine if there is a subgraph of H (the target graph) that is isomorphic to G (the pattern graph). Generally, the problem is NP-hard. I will present some simple SIP algorithms, all using BitSet encodings, and progressively modify a base algorithm to give more sophisticated algorithms that better exploit problem structure.

FATA Seminar - Life out on the Savannah: formal models meet mixed-reality systems (18 November, 2014)

Speaker: Michele Sevegnani

We report on work with our HCI friends, Tom Rodden and Steve Benford, on modelling and analysis for Benford’s Savannah mixed reality “game”.  We show how our novel bigraphical model of four perspectives of the system (computational, technical, human and physical), gives us new ways to analyse relationships between the perspectives and prove formally that there are cognitive dissonances in the system, as exemplified by user-trials.
No bigraph algebra required, we do everything with graphical forms (ie pictures)!
Formal modellers,  HCI experts, computer scientists, all welcome!