S-REPLS 20

Compositional symbolic execution (CSE) is a powerful technique for program verification and bug-finding, yet existing formal theories of CSE do not sufficiently bridge the gap between idealised models and real-world tools. We present mechanised progress towards a foundational, realistic, and end-to-end theory of CSE in the Rocq proof assistant. Our theory advances realism at both ends of the CSE pipeline: it supports an expressive frontend with algebraic data types, logical functions, and lemmas; it also provides a verified connection to SMT-LIB compliant SMT solvers. Our contributions include: (1) a CSE theory that captures practical verification patterns; (2) a standalone, reusable Rocq mechanisation of the SMT-LIB standard; (3) a proven-correct encoding from CSE backend queries to SMT-LIB queries that accounts for semantic discrepancies and optimises using type information; and (4) empirical evidence for the backend by extracting our verified SMT encoding and routing a sizeable fragment of solver queries from the CSE tool Gillian through it.

Continuations are a powerful programming concept: cooperative concurrency, coroutines, Python-style generators, and many other features can be implemented as libraries rather than being built into the language. Although delimited continuations have experienced renewed interest particularly because of the success of effect handlers, undelimited continuations, as offered by control operators in the call/cc family, fell out of fashion because of efficiency concerns and difficulty of reasoning. In this talk, we revisit undelimited continuations through the modern perspective of separation logic. We will see that this exploration indicates an alternative semantics of call/cc that is efficient, is compatible with powerful reasoning principles and itself enjoys surprisingly simple separation-logic reasoning rules, and can still be used to implement the usual applications of continuations. This is joint work with Xavier Leroy. It has been recently been conditionally accepted for publication at POPL 2027.

Message-passing concurrency is a common and well-explored approach to structuring programs that involve communication, but ensuring that communicating processes interact safely remains a challenging task. Behavioural type systems allow us to make progress towards this goal by describing not only the values communicated between processes but also the structure and format of the communication itself.

In this talk, I will compare and contrast two approaches to typing concurrent programs: mailbox types and session types. Mailbox types describe actor-based communication as in languages like Erlang and Elixir, describing messages that can be sent to or received from an actor’s mailbox using commutative regular expressions. In contrast, session types describe channel-based communication as in languages such as Go and Rust, and describe protocols of communication over a channel as a sequence of sends or receives. Traditionally, session types are linear, but we will also briefly look at graded session types which carefully relax this restriction to allow the programmer to encode non-linear communication patterns.

By examining these two models of communication and their respective typing disciplines, I aim to shed some light on their similarities and differences, and illustrate some of the contrasting challenges of precisely typing programs in each setting.

To be announced.

The design space for named parameters varies significantly between languages. Python, Scala, Swift, OCaml, etc. all make wildly different choices. We explore the design space, weigh trade-offs, and converge on best solutions for various goals (ergonomics, safety, ease of adoption).

RDMA provides fast communication by allowing machines to access remote memory directly, but its interaction with CPU weak memory and network ordering can produce subtle behaviours. For example, nodes may observe stale values even after polling for remote-write completion. The RDMA-TSO model formalises these behaviours.

This talk presents an extension of Dartagnan, an SMT-based bounded model checker for weak-memory programs, to support distributed RDMA systems. We add node-aware programs, RDMA events and relations, and the RDMA-TSO memory model. A two-node litmus test and tool demonstration show how Dartagnan can identify permitted RDMA behaviours and produce concrete witness executions.

We also discuss LOCO, a framework for building composable distributed objects over RDMA. LOCO specifies library correctness by relating implementations to memory-model specifications. We introduce Rochefort, a tool that build on Dartagnan to automate these soundness arguments, which are otherwise established through pen-and-paper reasoning, using litmus tests and SMT-based verification.

In transient execution attacks, such as Meltdown and Spectre, divergences from a program's expected control flow during execution can cause privileged information to be loaded and left in the microarchitectural state, which can be exploited by an attacker.

We present a semantic approach for detecting Spectre V1-type vulnerabilities (i.e. transient out-of-bounds loads) by taking a base language with established support for formal verification of epistemic predicates and adding support for speculative execution.

We apply program-to-program transformations to represent speculative execution and microarchitectural traces, and the leakiness of the resulting program can be automatically checked via an epistemic weakest precondition generator, mechanised epistemic to first-order translation, and SMT solver.

Reasoning about behavioural equivalence is key to the verification of reactive and infinite-state systems. A common pattern in proofs of correctness is to establish a simulation or abstraction relation between a rich, potentially unbounded source semantics and a finite transition system that captures its observable behaviour. Once such an abstraction is obtained, the remaining verification task often reduces to proving properties in the finite-state domain. Often, verification amounts to establishing (weak) bisimilarity between an abstraction of the source system and its specification. In practice, however, this final bisimulation step can still be unexpectedly demanding and rely on complex external tool support or substantial manual reasoning. We present a verification framework in Rocq, based on augmenting a standard bisimilarity-checking algorithm to produce (weak) bisimilarity proof terms in Gallina, directly applied to the proof through the Rocq API. Our automated bisimilarity proof is split into two parts: (1) extracting a graph from Rocq inductive propositions that represent the underlying (finite-state) abstraction of the system and its specification, and (2) running a proof-term generating bisimilarity-checking algorithm on these graphs. Together, these two steps correspond to a form of type-inhabitation procedure for statements of (weak) bisimilarity in Rocq. We implement these steps as a Rocq plugin, "rocq-mebi".