Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learning from automata to a large class of state-based systems, using the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems.

Joint work with Clemens Kupke and Simone Barlocco.

Beck's distributive laws provide sufficient conditions under which two monads can be composed, and monads arising from distributive laws have many desirable theoretical properties. Unfortunately, finding and verifying distributive laws, or establishing if one even exists, can be extremely difficult and error-prone.

We develop general-purpose techniques for showing when there can be no distributive law between two monads. Two approaches are presented. The first widely generalizes ideas from a counterexample attributed to Plotkin, yielding general-purpose theorems that recover the previously known situations in which no distributive law can exist. Our second approach is entirely novel, encompassing new practical situations beyond our generalization of Plotkin's approach. It negatively resolves the open question of whether the list monad distributes over itself.

Our approach adopts an algebraic perspective throughout, exploiting a syntactic characterization of distributive laws. This approach is key to generalizing beyond what has been achieved by direct calculations in previous work. We show via examples many situations in which our theorems can be applied. This includes a detailed analysis of distributive laws for members of an extension of the Boom type hierarchy, well known to functional programmers.

(Joint work with Dan Marsden)

Lenses are a popular approach to bidirectional transformations, a generalisation of the view update problem in databases, in which we wish to make changes to source tables to effect a desired change on a view. However, perhaps surprisingly, lenses have seldom actually been used to implement updatable views in databases. Bohannon, Pierce and Vaughan proposed an approach to updatable views called relational lenses, but to the best of our knowledge this proposal has not been implemented or evaluated to date. We propose incremental relational lenses, that equip relational lenses with change-propagating semantics that map small changes to the view to (potentially) small changes to the source tables. We also present a language-integrated implementation of relational lenses and a detailed experimental evaluation, showing orders of magnitude improvement over the non-incremental approach. Our work shows that relational lenses can be used to support expressive and efficient view updates at the language level, without relying on updatable view support from the underlying database.

Joint work with Rudi Horn and Roly Perera. Incremental relational lenses. Proc. ACM Program. Lang. 2, ICFP, Article 74 (July 2018), 30 pages. DOI: https://doi.org/10.1145/3236769

Multi-agent Systems (MAS) are distributed autonomous systems in which the components, or agents, act autonomously in order to reach private or common goals. MAS have been used as a paradigm to realise a wide number of applications ranging from autonomous systems and robotics to services, electronic assistants, and beyond. Logic-based specifications for MAS typically do not refer only to the agents’ temporal evolution, but also to their knowledge, strategic abilities, and other AI-inspired primitives.

I will begin by reporting algorithms for symbolic model checking against epistemic and strategic specifications. I will highlight potential speedups of these techniques via a number of techniques including symmetry reduction, parallel approaches, and SAT-based methods.

I will demonstrate MCMAS, an open-source BDD-based model checker supporting these specification languages. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicle will be discussed.

I will then consider the case of MAS where the number of agents is unbounded and cannot be determined at design time. This is a typical assumption in robotic swarms and recent internet of things applications. In view of solving this, I will report our approach to the parameterised model checking problem. While this is generally undecidable, I will present results that establish sufficient conditions for determining a cut-off of a MAS, i.e., the number of agents that need to analysed for verifying a MAS composed of any number of components. I concluded by presenting applications to the verification of related notions, such as emergence.

Rust is a new systems programming language, sponsored by Mozilla, that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features.

In this talk, I will present RustBelt (http://plv.mpi-sws.org/rustbelt), the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

After reviewing some essential features of the Rust language, I will describe the high-level structure of the RustBelt verification and then delve into detail about the secret weapon that makes RustBelt possible: the Iris framework for higher-order concurrent separation logic in Coq (http://iris-project.org). I will explain by example how Iris generalizes the expressive power of O'Hearn's original Concurrent Separation Logic in ways that are essential for verifying the safety of Rust libraries. I will not assume any prior familiarity with Concurrent Separation Logic or Rust.