The sixth edition of the Iris workshop will be held at ISTA in Vienna, Austria. It will be focused on Iris-related research, so as to allow for in-depth talks and discussions. The three-day-long program, with talks, extends from Monday, June 8 until Wednesday, June 10. Participants are encouraged to stay for one or two more days, on June 11 and June 12, for further informal discussions and interaction.
There will be lunch provided at the workshop and there will be an excursion followed by the workshop dinner. Details will follow.
Registration
Please register for the workshop via this website.
Registration costs 100 EUR and includes lunches, snacks, coffee, the workshop dinner, and the shuttle bus to and from ISTA.
The registration closes on May 8May 22. If you have questions about the registration, please contact the organizers.
If you wish to attend, we suggest registering now and booking accommodation as soon as possible, as Vienna in June can be very busy.
Program
This program is tentative and subject to change!
Monday (8 June)
| 08:30 | Shuttle bus from Schwedenplatz in Vienna to Moonstone Building |
|
|---|---|---|
| 09:00 | Welcome and coffee |
|
| 09:45 | Opening remarks |
|
| 10:00 |
Rini Banerjee:
Gradual Assurance for Systems Software: A Separation-Logic Approach (invited talk) [abstract]
The conventional code-test-debug cycle is the de-facto methodology for building software systems, and while successful to an extent, it manifestly fails to make these systems reliable enough. Various approaches have been explored over the past few decades that aim to ameliorate this, from push-button static and dynamic analysis tools to traditional formal verification via rich, explicit specifications. These specifications are costly to produce and maintain, especially at scale. Testing specifications concretely at runtime — as they are being written — can alleviate this, making it possible to check and debug in-progress, partial specifications in a lightweight manner, providing more gradual assurance. Unfortunately, the testing and proof communities have historically been largely disjoint, and much of the existing work in these areas focuses on a single approach and tool. We propose a more flexible use of rich specifications, written in a single assertion language, that can be refined as they are written using feedback from testing and property-based testing, and can eventually be used for proof, if desired. In this talk, I will describe our specification-testing-centred workflow, first abstractly and then instantiated to the systems software setting, using the CN separation-logic testing and verification toolchain [1]. I will explain how the component parts of the CN toolchain — runtime specification testing via Fulminate [2], property-based testing via Darcy [1] and Bennet [3], and proof via CN [4] — work. I will discuss our experience in leveraging CN to apply our workflow to a fragment of Google's pKVM hypervisor, and describe our work in running the Fulminate-instrumented fragment baremetal at the hypervisor privilege level, as part of pKVM. |
|
| 11:00 | Morning coffee break |
|
| 11:30 |
Thibaut Perami:
ArchSem: Formalising concurrent CPU architectures to support verification in Rocq
|
|
| 12:00 |
We present the implementation and mechanized verification of a realistic parallel scheduler for OCaml 5 using the Iris-based Zoo framework. Similarly to the Domainslib library, it relies on a work-stealing strategy to perform load balancing but also supports other scheduling strategies thanks to its flexible interface. We provide basic benchmarks demonstrating that its performance is on par with other schedulers from the OCaml ecosystem. As part of this effort, we verified the Chase-Lev work-stealing deque, as implemented in the Saturn library. |
|
| 12:30 |
Benjamin Peters:
TBD
|
|
| 13:00 | Lunch |
|
| 14:30 |
Session types statically guarantee that communication over a message-passing channel adheres to a protocol that specifies the types and order of the messages. However, standard session types assume that channels remain active until protocol completion---an unrealistic assumption, because threads often fail due to errors. We present an integration of session types with fine-grained error tracking. Unlike standard session types, our protocols do not only keep track of the type of messages that are exchanged, but also at which protocol steps the channel might be canceled with a corresponding error type. In a synchronized setting, fine-grained error tracking can be encoded using internal and external choice in standard session types. However, a naive adaptation to asynchronous channels with a semantics similar to Rust's mpsc channel library is unsound. We introduce the notions of error propagation and error stability to recover sound typing rules. We formally prove that our asynchronous version is sound by verifying end-to-end correctness w.r.t. a low-level lock-free channel implementation with a cancel operation. We also show that our work can be extended with polymorphism, recursive types, and dependent protocols in the style of the Actris framework. |
|
| 15:00 |
Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order languages, verifying it for higher-order languages with general references remains an open challenge. In such languages, operations may be used by arbitrary, unverified higher-order clients, making it unclear how to even define wait-freedom formally in terms of program semantics, let alone prove it. In this paper, we present the first framework for verifying wait-freedom of concurrent programs written in a higher-order language with general references. Our approach is based on the Lawyer concurrent separation logic which has been recently introduced for termination verification. We identify a specification pattern in the Lawyer logic that captures wait-freedom. To establish this connection formally, we prove a novel adequacy theorem for Lawyer which states that programs which are proven correct in the Lawyer logic against a specification in the aforementioned specification pattern are wait-free. As a part of proving the adequacy theorem above, we need to prove that the behavior of the client of the data structure is safe in the sense that it does not break the internal invariants of the data structure. To this end, we develop a logical relations model that establishes safety for all clients once and for all. We demonstrate the effectiveness of our approach by proving wait-freedom for several representative examples, including a higher-order list map function, and a memory-efficient single-producer, single-consumer queue. For the latter, wait-freedom is conditional in that, as the name suggests, there can be at most one enqueuer thread and one dequeuer thread. To capture this formally, we introduce the notion of restricted wait-freedom as a variant of wait-freedom that restricts the number of concurrent threads, and show how our approach can support reasoning about restricted wait-freedom. All our results have been mechanized with Rocq and Iris. |
|
| 15:30 | Afternoon coffee break |
|
| 16:00 |
Temporal Logic is suitable for verifying temporal properties, such as liveness: that something good eventually happens. For a multitude of temporal logics, the metatheory has been mechanised in a theorem prover, but none seem to focus on verifying actual examples, resulting in impractical verbosity primarily stemming from having to manually manage proof context. The lack of focus seems to be a consequence of temporal logics mostly being used in external automated tools, rather than mechanised proofs. As a result, mechanised proofs that rely on temporal properties (e.g. Trillium of the Iris ecosystem) must either (1) devise their own proof from scratch, or (2) be left with unsatisfactory holes in their proofs, relying on unmechanised translations to external tools. To address this concern, we propose the development of a proofmode specifically tailored towards temporal logic for verifying temporal properties or concrete examples. In this work (in progress), we use the Iris Proofmode (IPM) infrastructure to obtain a "non-Iris" proofmode (without resources or step indexing) for Linear Temporal Logic (LTL). The key insight is that LTL (and many other temporal logics) are based on modalities that bear resemblance to those already supported by the IPM. As a result, we can reuse patterns, for example, to eliminate modalities while keeping the proof context consistent. This is work in progress, and so the presentation will focus on the ongoing insights, challenges, and future directions, and happily receive feedback on those matters. |
|
| 16:30 |
Aaron Bies:
Extending Verus with Logical Atomicity
|
|
| 17:15 | Shuttle bus from Moonstone Building to Schwedenplatz in Vienna |
Tuesday (9 June)
| 08:30 | Shuttle bus from Schwedenplatz in Vienna to Moonstone Building |
|
|---|---|---|
| 09:00 | Welcome and coffee |
|
| 10:00 |
This talk presents the community effort to port Iris to the Lean theorem prover. We will give an overview of the past, the present and the future of Iris Lean port. Concretely, the talk will present a description of the advantages that the Lean version of Iris has to offer (paired with a list of challenges faced during the port), what the current status of the port is, how we maintain the connection of Iris Lean to Iris in Rocq and some insight into the projects that are already being built on top of Iris Lean. |
|
| 11:00 | Morning coffee break |
|
| 11:30 |
Tree Borrows is a new-ish aliasing model for Rust that improves over Stacked Borrows. As an aliasing model, it extends Rust's notion of Undefined Behavior (UB) by banning certain pointer aliasing patterns, which unlocks more compiler optimizations. But adding UB comes with a downside, namely that ensuring program correctness now also requires ruling out this additional UB. Currently, no existing Rust verification tool does this, and there is also no theoretical foundation for modular reasoning about Tree Borrows. We present our work-in-progress Separation Logic for Tree Borrows, built using Iris-Rocq. We describe its assertion language that allows modular reasoning about the tree, and we explain how the logic abstracts from the underlying tree, allowing for more efficient reasoning. |
|
| 12:00 |
This thesis presents a formalization of the core components of the Iris separation logic framework in the Arend theorem prover. Arend is a proof assistant based on homotopy type theory, a variant of dependent type theory. The formalization is based on the Rocq development of Iris and the paper “Iris from the Ground Up”. It implements an interface for bunched implications, ordered families of equivalences, complete metric resource algebras, uniform predicates, update mechanisms, weakest preconditions, and an adequacy theorem. |
|
| 12:30 |
Janine Lohse:
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation [abstract]
There has recently been exciting progress in the realm of probabilistic separation logics. An important subclass of these—including PSL, Lilac, Bluebell, and pcOL—are general-purpose probabilistic logics (or GPLs, for short), meaning that they provide primitive Hoare-style assertions about probability distributions on the program state, along with powerful modularity principles like independence and conditioning. However, none of these logics support reasoning about dynamically allocated memory (i.e., pointers into a heap), let alone the more sophisticated resource algebra-based ghost state of modern separation logics like Iris. We argue that this is due to a fundamental obstacle: since the shape of memory (and identity of memory locations) may differ under different random outcomes, it is unclear how pointer ownership can be harmonized with probabilistic independence and conditioning. In this talk, I will describe our substantial first steps towards a marriage of GPLs and modern separation logics like Iris, in the form of Amaryllis. Amaryllis is the first GPL to support independence and conditional reasoning while also handling dynamic memory allocation. To overcome the aforementioned obstacle, we developed a new indexed valuation-style model of probabilistic assertions, whereby ownership of a standard Iris-style resource (e.g., heaps) can be promoted to ownership at the level of distributions in a generic fashion. |
|
| 13:00 | Lunch |
|
| 14:00 |
Eugène Flesselle:
Effectful Program Transformations
|
|
| 14:30 |
This talk presents a separation logic framework, heavily inspired by Iris, for concurrent programs, that allows reasoning about both affine and linear resources, as well as affine and linear invariants. Moreover, the logic supports thread-local and thread-shared invariants, allowing thread-local ones to be opened for more than one step of computation, before reaching a yield-point (such as the "await" keyword), through an extended version of the fancy update modality. We devised a weakest precondition to reason about asynchronous programs (with threads and asynchronous tasks in each thread), proved its adequacy, and showed leak freedom with respect to linear resources. All results are fully mechanized in Rocq. |
|
| 15:00 | Excursion and workshop dinner |
Wednesday (10 June)
| 08:30 | Shuttle bus from Schwedenplatz in Vienna to Moonstone Building |
|
|---|---|---|
| 09:00 | Welcome and coffee |
|
| 10:00 | ||
| 11:00 | Morning coffee break |
|
| 11:30 |
End-to-end full-stack verification requires a powerful reasoning framework to tackle concurrency and prove higher-order properties about hardware such as processors, networks-on-chip and AI accelerators. This reasoning needs to connect smoothly to the software running atop to finally form an end-to-end proof. In our current project, we build a system that runs a unikernel operating system on top of a RISC-V processor. To reason at the hardware level, we instantiate Iris with Kôika, a high-level hardware description language in Rocq with a formally-verified compiler to SystemVerilog. In this talk, we introduce our current instantiation, present a first use case and show our vision of connecting software and hardware via this Iris instance. |
|
| 12:00 |
Niklas Mück:
TBD
|
|
| 12:30 |
Alexander Loitzl:
Multi-language Program Logics
|
|
| 13:00 | Lunch |
|
| 14:30 |
Traditionally, proof systems such as program logics come with two core theorems: soundness and completeness. The role of soundness is obvious: we want to be sure that arguments carried out inside the logic actually lead to correct conclusions. Completeness complements that by ensuring that the logic does not limit expressivity: in principle, any correct result can be obtained within the confines of the logic. This result typically has to be stated relative to the completeness of the assertion logic that is used to reason about pre- and postconditions. Over the past decade, the Iris framework has emerged as a widely used foundation for building separation logics. While Iris-based logics typically come with a soundness proof, none of them come with a proof of completeness. In fact, it is not entirely clear how to translate the typical recipe for relative completeness to Iris-based logics: the languages these logics reason about are typically higher-order, enabling forms of recursion that go beyond a simple while loop (e.g., Landin's Knot). In the first part of this talk, I will present our approach for establishing completeness of Iris-based program logics, and show the generality of our methodology by applying it to a range of different logics described in prior work, including partial and total logics for Iris HeapLang, and a CaReSL-style relational logic. In the second part, I will present our follow-up ongoing work on the completeness of logically atomic triples in Iris, and discuss how completeness enriches Iris-based logics by enabling embedding results of external techniques into Iris. |
|
| 15:00 |
Arnaud Daby-Seesaram:
SIrIS: Mechanised Verification of a Key-Value Store Library satisfying Snapshot Isolation [abstract]
Isolation Levels in the database jargon define how much transactions can observe and how much they can interfere with one another. Among them, Snapshot Isolation is particularly popular because it allows concurrent transactions to take place while providing strong enough guarantees for most use cases (e.g., it precludes write-write conflicts between concurrent transactions and ensures causal consistency). Previous work has shown how to efficiently implement this isolation level using multi-version concurrency control. Other previous work provides Separation Logic specifications for Snapshot Isolation. However, currently verified implementations are inefficient and only use coarse-grained concurrency control. In this talk, I will introduce SIrIS, a library providing single-node in-memory databases satisfying Snapshot Isolation. It uses fine-grained concurrency control and provides a GC to limit its memory usage. I will first show our specification and how to use it on a small client example. Second, I will discuss implementation of the library and its performance. Our results are formalised in the Rocq Prover using the Iris framework. This is joint work with Léon Ducruet, Amin Timany and Lars Birkedal. |
|
| 15:30 | Afternoon coffee break |
|
| 16:00 |
Robbert Krebbers and Ralf Jung:
Session with Iris Maintainers
|
|
| 16:45 | Closing remarks |
|
| 17:15 | Shuttle bus from Moonstone Building to Schwedenplatz in Vienna |
Thursday (11 June) – Friday (12 June)
- Discussion groups and meetings organized by attendees.
Location: Moonstone Building, ISTA campus near Vienna
The workshop will be held on the campus of Institute of Science and Technology Austria (ISTA), located in Klosterneuburg, Austria. Klosterneuburg is a historical town in Lower Austria, 20 minutes from Vienna. More information about the city and visitor information, can be found on the official website of the town.
The conference will take place in the Moonstone Building in the Seminar Center.
Daily shuttle from Vienna to the ISTA campus
The workshop takes place in the Moonstone Building on the ISTA campus in Klosterneuburg, just outside Vienna. We recommend staying in Vienna and using the free daily shuttle bus to reach the ISTA campus in the morning and return to Vienna in the evening.
Shuttle bus (free of charge)
- Morning shuttle: 08:30 from Schwedenplatz in Vienna towards ISTA.
- Evening shuttle: 17:00 from ISTA towards Schwedenplatz in Vienna.
- Additional stops: U4 Heiligenstadt and Stadtplatz in Klosterneuburg.
Public transportation (Klosterneuburg)
You can also reach Klosterneuburg by public transport, in particular by bus 400 and train S40. Use the VOR route planner to find connections. Tickets bought directly on the bus require cash. Buses and trains from Vienna to Klosterneuburg run until around midnight.
Hotels near the shuttle stops
We recommend staying near one of the conference shuttle stops: Schwedenplatz in Vienna, Heiligenstadt in Vienna, or Stadtplatz in Klosterneuburg. Vienna is usually the most convenient option because it has more hotels, restaurants, and evening options. The hotels below are within walking distance of one of the shuttle stops.
Vienna:
- Kärntnerhof (from 95 EUR per night for a single room, 5 min to bus stop Schwedenplatz)
- Hotel Ruby Lissi (from 120 EUR per night, 5 min to bus stop Schwedenplatz)
- Hotel Mercure Wien Zentrum (from 120 EUR per night for a double room, 5 min to bus stop Schwedenplatz)
- SO/ Vienna (from 225 EUR per night for a double room, 5 min to bus stop Schwedenplatz)
- Hotel Stefanie (from 272.50 EUR per night for a double room, 5 min to bus stop Schwedenplatz)
Klosterneuburg:
- Hotel Anker (from 76 EUR per night, 5 min to bus stop Klosterneuburg)
- Bed and Breakfast “Alte Mühle” (69 – 96 EUR per night for a single room, 10 min to bus stop Klosterneuburg)
- Hotel Schrannenhof (from 98 EUR per night, 5 min to bus stop Klosterneuburg)
- ISTA Guesthouse (47 - 70 EUR per night depending on the room type, located on the ISTA campus.)
Hotel map: if the embedded map does not work, you can view it directly in Google Maps.
Organizers
Scientific organizers:
- Michael Sammler (ISTA, Austria), email: michael.sammler@ista.ac.at
- Jules Jacobs (Jane Street), email: julesjacobs@gmail.com
- Alexander Salzmann, email: alexander.salzmann@ista.ac.at
- Maresa Wiener, email: maresa.wiener@ista.ac.at