Invited Talks

Simon Chadwick : Formal Verification - The Journey from Theory towards Practice
This presentation will look at the steps we have taken towards practical verification of railway signalling interlocking logic using formal verification. The theory is well demonstrated, and we have been working on some steps towards a system for use by railway signalling engineers. Some of the issues we will consider: How to convey understanding about formal verification - what is checked, what is not checked; How to express safety properties; How to capture railway geography; How to provide a User Interface; How to present the results; How would formal verification fit within the overall process for interlocking data.
Robert Constable : Implementing elements of intuitionistic mathematcs in Nuprl
There is no way to implement all of intuitionistic real analysis or even formalize it. Brouwer, the primary creator of intuitionistic mathematics, knew this and said that a construction of the continuum is inconceivable. We will explain in this lecture why that is so. This is not the case for the Bishop and Bridges account of constructive analysis. Dr. Mark Bickford has implemented significant parts of constructive analysis in Nuprl. It might be possible to implement the entire book. Bishop's comment on Brouwer's view is priceless, and perhaps not well known. The lecture will use Bishop's written remark as motivation and then discuss how we are implementing elements of intuitionistic mathematics in Nuprl.
Edith Elkind : Hedonistic diversity games
We consider a setting where players belong to two types (men and women, vegetarians and carnivores, junior and senior researchers) and need to split into groups, with each player having preferences over the proportion of the two player types in his or her group. We study the problem of finding a stable partition, for several game-theoretic notions of stability; while some of the problems we consider turn out to be polynomial-time solvable, others are NP-hard, in which case we also explore their parameterized complexity.

David Manlove : Assigning junior doctors to hospitals - what makes it so hard?
In many countries, junior doctors are assigned to hospitals via a centralised matching process. Algorithms take as input the preferences of doctors over hospitals and vice versa, and the upper quotas of hospitals (these are the numbers of doctors that each hospital has room for). The algorithms typically produce stable matchings of doctors to hospitals, which guarantee that no doctor and hospital would rather be assigned to one another than to remain with their existing assignee/s (if any). The underlying computational problem has been well studied in its classical form, and fast algorithms are known for finding stable matchings. In this talk we focus on extensions of the classical problem of assigning junior doctors to hospitals that are motivated by practical applications, each of which leads to an NP-hard problem. Variants that we consider include, for example: (i) trading off size with stability, where we seek larger matchings that minimise instability; (ii) allowing ties in the preference lists; (iii) allowing couples to apply jointly to pairs of hospitals that are typically geographically close; (iv) allowing hospitals to have lower quotas as well as upper quotas. In each case we motivate and define the problem, survey existing algorithmic results and outline some open cases.

Patrick Totzke : Playing with counters: how to solve games on infinite arenas
I will talk about perfect information zero-sum games played on graphs, which are ubiquitous in formal verification of reactive systems. For instance, solving (i.e., determining the winner of) parity games is equivalent to model checking for modal μ-calculus formulae, which in turn subsumes both LTL and CTL specifications. Let’s ignore for now that the complexity of solving Parity games remains unknown and instead be greedy and look into more expressive types of games. Moving from finite graphs to infinite ones and introducing randomization allows to study interesting interplay between the structure of the graphs, the complexities of winning strategies, and the decidability/complexity of game solving. It turns out that many interesting generalizations effectively reduce to solving so-called energy games, in which one of the two players simply wants to keep a discrete “energy” level nonnegative. In this talk I will recall historical and recent results on such games played on infinite graphs and point to open problems in the area.
Kristina Vušković : The induced disjoint paths problem on (theta, wheel)-free graphs
A hole in a graph is a chordless cycle of length at least 4. A theta is a graph formed by three internally vertex-disjoint paths of length at least 2 between the same pair of distinct vertices. A wheel is a graph formed by a hole and a node that has at least 3 neighbors in the hole. In joint work with Trotignon and Radovanović we obtain a decomposition theorem for the class of graphs that do not contain as an induced subgraph a theta nor a wheel, using clique cutsets and 2-joins. In this talk we show how this decomposition theorem can be used to solve the induced disjoints paths and related problems on this class.

Contributed Talks


SPONSORS

BCTCS Logo London Mathematical Society Logo Heilbronn Institute for Mathematical Research Logo AlgoUK Logo Technocamps Logo Institute of Coding Logo SonyUK Logo