Rigorous Systems Seminar

After the 6th July talk we will have a break until mid-August.

Upcoming Talks

• 6 July 2026

  Speaker: Janis Bailitis

  Title: Towards Quantitative Logics in Rocq

  Abstract

  Quantitative logics (QLs) are logics whose truth values go beyond 0 and 1. Notable examples include fuzzy logics interpreted in [0,∞], which give propositions like "x is much larger than 10" a meaningful truth value. Despite growing importance, for example in verification of machine learning, QLs lack a general formal theory. Addressing this issue, inspired by a Rocq mechanisation of selected QLs due to Affeldt et al., we envisage a general and reusable library for QLs mechanised in Rocq, containing the previous mechanisations as case studies.

  In this talk, we will briefly present the proposed structure of the library with a focus on intervals of real numbers, a key ingredient to many QLs, mechanised using the MathComp-analysis library. Then, we will discuss work in progress on mechanising Quantitative Linear Logic within our library, which is a recently proposed QL by Capucci et al. generalising multiplicative-additive linear logic.

  
  

Past Talks

• 22 June 2026

  Speaker: Mathews George

  Title: A Tactic for Pattern Matching in Autosubst

  Abstract

  Reasoning about binders in a proof assistant requires additional overhead compared to paper-based proofs. Autosubst enables automatic equality-checking up to the σ-calculus for assumption-free equalities, allowing users of proof assistants to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without β-reduction, solutions of matching may not be unique. In this talk, we present a work-in-progress method for automatically pattern matching against assumptions evaluated on standard case studies, including the benchmarks POPLMark and POPLMark Reloaded challenges.
  
  
• 22 June 2026

  Speaker: Yukang Xie

  Title: A Dataflow-Driven Processor for Lazy Functional Programming Languages

  Abstract

  Specialised hardware for functional languages has a long history, driven by the hope of running expressive languages like Haskell more efficiently than conventional machines allow. Recent designs have made progress, but they share a stubborn limitation: the natural way to run these programs - graph reduction - is sequential, with each step depending on the last. This makes it hard to speed things up through pipelining.

  This talk presents Ouros, a processor that takes a different approach. Instead of a central logic deciding what happens next, processor components work in a data-driven manner. Ouros also splits work into lightweight threads automatically, without help from the programmer or compiler - something that was previously impractical because managing threads cost too much. In Ouros, creating and synchronising a thread each take a single cycle.

  I'll also describe the garbage collector, which cleans up memory in the background, with its algorithm verified by bounded model checking, and close with results from simulation and FPGA prototyping.

  
  
• 15 June 2026 at 11am in IF G.03, University of Edinburgh

  Speaker: Sophie Pinchinat (IRISA, Université de Rennes)

  Title: A Journey Through the Formal Aspects of Attack-Defence Trees

  Abstract

  Attack-defence trees (ADTs) are classical graphical models to reason about a hierarchical decomposition of a main attack goal into a combinations of sub-goals (that are in turn decomposed, and so on). ADTs are one of the oldest method to conduct risk analysis that is still highly recommended, e.g. by NATO, but also by the National Cyber Security Centre of the UK Government, as they help security experts to exhibit optimal countermeasures to protect the system under study/design.

  Originally, ADTs have been constructed manually in a highly informal manner: the node labels are plain textual descriptions of what the expert has is mind, and the meaning of sub-goal combinators (classically OR, AND and sequentialAND) is left open to the designer intuitive interpretation. The academic world has developed various formal settings to better handle ADTs, hoping for diverse (semi-)automated techniques.

  In this talk, we focus on a piece of work, started a decade ago, that shows formal approaches to assist experts in constructing ADTs, with an accurate account of the computational complexity of decision problems relevant to the use of ADTs in practice.

  
  
• 8 June 2026

  Speaker: Freya Murphy (University of Surrey)

  Title: Verifying Account Ecosystems with Graph Transformations

  Abstract

  Account ecosystems comprise a set of resources, including online accounts, devices, and credentials, that jointly impact a user's or organisation's security. Prior work shows that users frequently overlook subtle dependencies within these ecosystems, leading to security breaches that are difficult to detect using analysis techniques focused on isolated components.

  This talk introduces resource access graphs (RAGs), a formal model for the automated analysis of dynamic account ecosystems. To capture the dynamic nature of account ecosystems, we define a transition system based on graph rewriting with RAGs as states in which both user actions and adversarial capabilities are modelled as graph transformation rules. Security properties are specified in computation tree logic (CTL), allowing automated analysis.

  The approach is demonstrated on a simple Apple account ecosystem with the recent security feature Stolen Device Protection (SDP). The analysis reveals limitations in SDP, affecting both the integrity and availability of a user's Apple Account.