Arnaud Daby-Seesaram

Contact Information.

Email

firstname.last-name@cs.au.dk

Office

Bygning 5341 (Turing building), office 126

Research Interests

I am interested in programming language semantics, and software verification using Separation Logic.

As part of my PhD, I study databases, and guarantees they provide to applications. To improve performance, database systems allow concurrently running transactions. However, the more concurrency is allowed, the less data consistency is guaranteed. To ensure correctness of applications, we need to ensure that they do not assume more consistency than guaranteed by the database.

Consistency guarantees of databases are formally captured by consistency- and isolation-levels. During my PhD, I focus on two flavours of Snapshot Isolation: Strong Snapshot Isolation, and Strong Session Snapshot Isolation.

Publication and talks.

• Verified Key-Value Stores Satisfying Snapshot Isolation
  By A. Daby-Seesaram, L. Ducruet, L. Birkedal, A. Timany.
  Venue: Symposium on Consistency Checking Principles 2026.
  

• SIrIS: Mechanised Verification of a Key-Value Store Library satisfying Snapshot Isolation
  By A. Daby-Seesaram, L. Ducruet, A. Timany, L. Birkedal.
  Venue: Iris Workshop 2026.
  

  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.

  
  
• Osiris: an Iris-based program logic for OCaml.
  By A. Daby-Seesaram, F. Pottier, A. Guéneau.
  Venue: OCaml Workshop 2023.
  [slides] [code] [video]

  abstract

  Osiris is a project that aims to help OCaml developers verify their code using Separation Logic. The project is still young: we currently only support a subset of the features of the OCaml language, including modules, mutual recursion, ADTs, tuples and records. Ultimately, we would like to extend Osiris to support most features of the OCaml language. Iris is a Coq framework for Separation Logic with support for expressive ghost states. It is often used to define program logics and can be parameterized by a programming language — usually described by its small-steps semantics. Most Iris instantiations target ML-like languages, each focusing on a specific purpose and lacking support of programming features such as records or ADTs. Osiris contains an Iris instantiation with a presentation of the semantics of OCaml, in order to reason on realistic OCaml programs. Osiris provides a translation tool to convert OCaml files to Coq files (cf. section 2). In order to verify an OCaml program with Osiris, one would use the translator on an OCaml file, seen as a module. This produces a Coq file containing a deep-embedded representation me of the module. The user would then write and prove a specification for the interpretation of me in our semantics.

  
  
• Modular Verification of State-Based CRDTs in Separation Logic
  By A. Nieto, A. Daby-Seesaram, L. Gondelman, A. Timany, L. Birkedal.
  Venue: ECOOP 2023.
  [code]

  abstract

  Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTS, while respecting the desiderata (a)–(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.

  
  

Education.