LogSem Seminar talks in 2025
06-01-2025: Extending Iris with liveness reasoning
Speaker: Egor Namakonov, Aarhus University
Time: 13:00-14:00
Location: Nygaard-297
Abstract: Higher-order program logics like Iris have proven extremely expressive for the verification of safety properties. However, the same level of expressivity for liveness verification is yet to be achieved. The existing work in this area had to compromise either on higher-order reasoning, compositionality, verifying the whole development foundationally, or being language-agnostic. In this talk, I’ll give an overview of a few Iris developments that deal with liveness verification. Then, I’ll introduce Lawyer - our ongoing project aiming at achieving all of the aforementioned goals - and show how to use it to verify the termination of a simple concurrent program.
10-02-2025: Efficient simulation of High-Level Quantum Software
Speaker: Adam Husted Kjelstrøm, Aarhus University
Time: 13:00-15:00
Location: Ada-333
Abstract: Simulation is a natural way to investigate program behavior. Interestingly for the quantum setting, a single simulation is enough to determine equivalence between programs, making simulation algorithms powerful tools for verifying program correctness. Practical quantum computing is hampered by the high error rates of instructions. To improve practical performance, code minimizers are employed. In this setting, Simulators can be paired with heuristic search to equivalence check candidate smaller programs. To build such code minimizers, efficient simulation algorithms are crucial. In this presentation, I will introduce a simulator for high-level quantum software. Other simulators compile the user-provided code to a low-level representation before simulating, resulting in increased software size and an (exponential) blow-up in simulation time. By directly simulating high-level code, this overhead is avoided, resulting in efficient simulation of certain classes of quantum software.
It is natural to ask whether all quantum code can be efficiently simulated. Assuming SETH, I demonstrate how some quantum code can never be efficiently simulated. Specifically, access to even a single ADD instruction is enough to encode 3SAT.
24-02-2025: Gradual typing, for the love of dynamic!
Speaker: Koen Jacobs, INRIA
Time: 13:00-15:00
Location: Ada-333
Abstract: Gradual typing has long been advocated as a means to bridge the gap between static and dynamic type disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, or making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, amongst which the refined criteria by Siek et al.
In this talk, we start out by introducing a concrete and realistic running example to exemplify the aforementioned use-cases, with which we then present some basic ideas behind gradual typing as they are presented in the literature. Moreover, we shall use an intuitive expectation of this example to extract a novel formal criterion about the general use-cases, inspired by the literature on secure compilation.
As we shall see, the novel criterion imposes an upper bound on how quickly a cast error may occur when importing dynamically-typed code at a particular static type. Informally, if a dynamically-typed program is semantically well-behaved at a static type, importing that program into the gradual language at said type should result in a gradual program that cannot ever (under arbitrary interaction) be responsible for a cast error.
We shall demonstrate that this novel criterion is not implied by any of the existing meta-theoretical properties of gradual languages, highlighting four concrete counter-examples from the literature. Additionally, we report on a fully formalized proof in the Coq/Rocq proof assistant (using the Iris library) that this property is satisfied within an appropriate setting of a gradualized simply typed lambda calculus.
03-03-2025: Formal verification of capability machine properties
Speaker: June Rousseau
Time: 13:00-15:00
Location: Ada-020
Abstract: In this talk, I will present the two main projects of my PhD, related to verification of capability machine (CHERI) properties. In a first part, I will present our formalisation of CHERIoT, an adapted architecture CHERI for IoT devices. I will explain how our new logical relation supports the mutually distrusful compartmentalisation model of CHERioT. In a second part, I will present how we plan to verify CHERI-TrEE, an extension of CHERI for trusted execution enclaves. More specifically, I will present you one of the main challenges we encounter when formalising CHERI-TrEE in Iris.
10-03-2025: Implementing the transitive closure of a step-indexed logical relation
Speaker: Laurits Bligaard
Time: 13:00-15:00
Location: Nygaard-298
Abstract: In this talk, I will discuss the implementation details of the transitive closure of a logical relation in Coq. Step-indexed logical relations are in general difficult to prove transitive. Instead there have been various suggestions on how to construct them such that they enjoy transitivity. One such approach is to define a new relation as essentially the transitive closure of a step-indexed logical relation. Last semester, I read up on logical relations and their formalization in Coq. As an end-of-the-semester project I implemented such a transitive closure of a step-indexed logical relation defined in Iris. I will present the details and considerations I had when adapting the general transitive-closure approach to a Iris-specific relation defined in Coq.
24-03-2025: Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
Speaker: Sergei Stepanenko
Time: 13:00-15:00
Location: Nygaard-297
Abstract: Recursive domain equations are omnipresent in the study of programming languages, particularly in semantical models for languages with higher-order functions. While existing approaches trade off expressive power to be more amedable to mechanization, certain more expressive frameworks, such as the topos of trees, have remained primarily theoretical and lack mechanized formalization.
In this talk, I will present joint work with Amin Timany on the formalization of solutions to guarded domain equations in the category of presheaves over ordinals using the Rocq proof assistant. We address the challenges posed by previous approaches, particularly in handling transfinite step-indexing and sheaves. By simplifying previous constructions from the setting of sheaves to presheaves, we implement more user-friendly framework while preserving expressivity. I will discuss key technical insights, limitations of existing mechanizations, and the refinements that enabled a usable formalization.
31-03-2025: Proving the core security theorem for the TLS-1.3 Key Schedule
Speaker: Lasse Letager Hansen
Time: 13:00-15:00
Location: Ada-020
Abstract: In this talk we will look at how to prove security properties for the TLS-1.3 Key Schedule. This work is part of a larger effort for proving correctness and security of Bertie a TLS-1.3 implementation. The protocol is implemented in Rust, and translated into SSProve, F*, and ProVerif using the Hax framework. These parts the validate different properties of the protocol. The security proof is based on an existing pen and paper proof in the State Seperating Proof (SSP) style. We will discuss how to construct such proof for a large protocol and the difficulties of formalizing it.
14-04-2025: Simulating quantum computers: the basics
Speaker: Adam Husted Kjelstrøm
Time: 13:00-15:00
Location: Ada-333
Abstract: Modern quantum hardware is severely resource constrained, meaning any near-term practical quantum software must be similarly economical. When minimizing resource consumption, validating program correctness is crucial, something which can be achieved by simulating the quantum software on a classical computer. In this presentation, I will introduce the basics of quantum computation. Then I will present four different algorithms for simulating quantum software, and discuss their respective advantages and disadvantages.
22-04-2025: On the univalence axiom
Speaker: Daniel Gratzer
Time: 12:00-13:00
Location: Nygaard-395
Abstract: This is an expository talk about the centerpiece of homotopy type theory: the univalence axiom. We try to describe where the univalence axiom came from, its precise statement, and why it’s nothing to be (too) afraid of. Along the way, the hope is to illustrate a few of the features and ideas that go hand-in-glove with univalence: higher inductive types, the structure-identity principle, and (the statement of) descent. This talk is aimed at people with a reasonable working knowledge of type theory (perhaps through interaction with a proof assistant) but we will try and keep the discussion informal. In particular, not too much discussion of particular Γ and ⊢ rules and certainly not too much homotopy theory!
28-04-2025: Context-Dependent Effects in Guarded Interaction Trees
Speaker: Amin Timany
Time: 13:00-15:00
Location: Ada-333
Abstract: Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called “bind rule” in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.
05-05-2025: First-order store and visibility in the π-calculus
Speaker: Iwan Quémerais
Time: 13:00-15:00
Location: Ada-333
Abstract: The π-calculus is the paradigmatic name-passing calculus. While being purely name-passing it allows the representation of higher-order functions and store. What it means for a computation to only involve storage of first-order values is unclear for π-calculus processes. I will present how we can nonetheless enforce this discipline with a type system inspired by the notion of visibility, coming from game semantics, in the case where computation is sequential. Then, I will discuss the impact of visibility on the behavioural theory.
07-05-2025: Pragmatic Test-oracle Specification of a Production Hypervisor
Speaker: Kayvan Memarian
Time: 10:00-12:00
Location: Ada-333
Abstract: Developing systems code that robustly provides its intended security guarantees remains very challenging: conventional practice does not suffice, and full functional verification, while now feasible in some contexts, has substantial barriers to entry and use.
In this work, we explore an alternative, more lightweight approach to building confidence for a production hypervisor: the pKVM hypervisor developed by Google to protect virtual machines and the Android kernel from each other. The basic approach is very simple and dates back to the 1970s: we specify the desired behaviour in a way that can be used as a test oracle, and check correspondence between that and the implementation at runtime. The setting makes that challenging in several ways: the implementation and specification are intertwined with the underlying architecture; the hypervisor is highly concurrent; the specification has to be loose in certain ways; the hypervisor runs bare-metal in a privileged exception level; naive random testing would quickly crash the whole system; and the hypervisor is written in C using conventional methods. We show how all of these can be overcome to make a practically useful specification, finding a number of critical bugs in pKVM along the way.
This is not at all what conventional developers (nor what formal verifiers) normally do – but we argue that, with the appropriate mindset, they easily could and should.
19-05-2025: A step-indexed denotational semantics of Call-by-push-value with arbitrary recursive types in the category of COFEs
Speaker: Virgil Marionneau
Time: 13:00-15:00
Location: Ada-333
Abstract: In this talk I will discuss a Coq formalisation of a denotational semantics for Levy’s Call-by-push-value extended with arbitrary recursive types. Similar work has been done synthetically for FPC by R. Møgelberg and M. Paviotti for FPC using extensional gDTT as a meta-theory. However to this day no pratical implementation of this theory exists inside a proof-assistant. For this reason we decided to work analytically inside the category of Complete Ordered Family of Equivalences of which a shallow embedding is already formalized in Coq as a means to provide a model to the Iris program logic.
26-05-2025: Coneris: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Speaker: Kwing Hei Li
Time: 13:00-13:30
Location: Ada-333
Abstract: How does one reason about programs that involve both concurrency and probability? In this talk, we will look at examples of concurrent probabilistic programs, each of increasing complexity, and I will show how to use Coneris, a mechanized program logic, to verify error bounds for these examples. A central novelty of Coneris is that it utilizes presampling tapes and a probabilistic update modality to describe how state is changed probabilistically at linearization points, which captures the notion of randomized logical atomicity. Together with other logical facilities such as error credits, ghost states, and invariants, we will see how Coneris support modular reasoning about error bounds for concurrent probabilistic modules.
26-05-2025: Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
Speaker: Egor Namakonov
Time: 13:40-14:10
Location: Ada-333
Abstract: Iris has been successfully used to verify a variety of safety properties. However, attempts to verify liveness with it so far had to compromise on either impredicativity, modularity or being mechanized in Rocq. In this talk, we introduce Lawyer — a program logic for modular verification of fair and unfair termination. It draws inspiration from the two previous lines of work: verifying termination in a higher-order language instrumented by erasable ghost code (most recently exemplified by Sassy) and proving refinement of a purely logical transition system (implemented by Trillium). We demonstrate the modularity of Lawyer by showing termination of a client program of a fair lock module. To the best of our knowledge, Lawyer is the first mechanized program logic that supports modular, impredicative, liveness-aware specifications of modules.
26-05-2025: Iris-Wasm: formally establishing a robust and modular program logic for WebAssembly and its proposed extensions
Speaker: Maxime Legoupil
Time: 14:20-14:50
Location: Ada-333
Abstract: WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher-order modular programming. We introduce Iris-Wasm (PLDI'23), a mechanised higher-order separation logic building on a specification of Wasm 1.0 mechanised in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby formally demonstrating that WebAssembly enforces strong isolation between modules. Iris-Wasm is also an optimal starting point to formally reason about extensions to WebAssembly, such as MSWasm (we introduce Iris-MSWasm at OOPSLA'24) and Stack-Switching/WasmFX (Iris-WasmFX is a work in progress). Formally describing and proving the desired properties of these extensions is a strong asset in validating them and encouraging their adoption.
02-06-2025: AWDIT: An Optimal Weak Database Isolation Tester
Speaker: Lasse Møldrup
Time: 13:00-14:00
Location: Ada-333
Abstract: In order to achieve low latency, high throughput, and partition tolerance, modern databases forgo strong transaction isolation for weak isolation guarantees. However, several production databases have been found to suffer from isolation bugs, breaking their data-consistency contract. Black-box testing is a prominent technique for detecting isolation bugs, by checking whether histories of database transactions adhere to a prescribed isolation level.
In order to test databases on realistic workloads of large size, isolation testers must be as efficient as possible, a requirement that has initiated a study of the complexity of isolation testing. Although testing strong isolation has been known to be NP-complete, weak isolation levels were recently shown to be testable in polynomial time, which has propelled the scalability of testing tools. However, existing testers have a large polynomial complexity, restricting testing to workloads of only moderate size, which is not typical of large-scale databases.
In this work we develop AWDIT, a highly-efficient and provably optimal tester for weak database isolation. Given a history $H$ of size $n$ and $k$ sessions, AWDIT tests whether $H$ satisfies the most common weak isolation levels of Read Committed (RC), Read Atomic (RA), and Causal Consistency (CC) in time $O(n^{3/2})$, $O(n^{3/2})$, and $O(n \cdot k)$, respectively, improving significantly over the state of the art. Moreover, we prove that AWDIT is essentially optimal, in the sense that there is a conditional lower bound of $n^{3/2}$ for any weak isolation level between RC and CC. Our experiments show that AWDIT is significantly faster than existing, highly optimized testers; e.g., for the $\sim$20% largest histories, AWDIT obtains an average speedup of $245\times$, $193\times$, and $62\times$ for RC, RA, and CC, respectively, over the best baseline.