Program

We are happy to announce invited talks by:

• Travis Hance: Leaf: A composable theory of shared resources as a basis for efficient systems verification
• Upamanyu Sharma: Verifying distributed systems using Grove

Monday (2 June)

• 08:30-09:00: Coffee
• 09:00-10:00: Invited talk: Upamanyu Sharma (MIT): Verifying distributed systems using Grove [abstract]
  Implementing distributed systems correctly is difficult. They deal with concurrency, network unreliability, reconfiguration, crash recovery, leases, etc. Grove is a framework for formally verifying distributed systems implemented in Go and supports reasoning about all these aspects and their interactions. By building on Iris, Grove provides ghost resources and invariants to reason about distributed protocols, introduces time-bounded invariants to reason about leases, uses logical atomicity to help specify distributed system components, and more. We used Grove to verify case studies consisting of several distributed systems components, including libraries for primary/backup replication, lease-based client key-value caching, Paxos, and durable storage. These case study systems achieve reasonable performance, including a read-only operation optimization based on leases.
• 10:00-10:30: Coffee
• 10:30-11:00: Kimaya Bedarkar (MPI-SWS): RefinedProsa: connecting response-time analysis with C verification for interrupt-free schedulers [abstract]
  There has been a recent upsurge of interest in formal, machine-checked verification of timing guarantees for C implementations of real-time system schedulers. However, prior work has only considered tick-based schedulers, which enjoy a clearly defined notion of time: the time "quantum". In this work, we present a new approach to real-time systems verification for interrupt-free schedulers, which are commonly used in deeply embedded and resource-constrained systems but which do not enjoy a natural notion of periodic time. Our approach builds on and connects two recently developed Rocq-based systems -- RefinedC (for foundational C verification) and Prosa (for verified response-time analysis) -- adapting the former to reason about timed traces and the latter to reason about overheads. We apply the resulting system, which we call RefinedProsa, to verify Rössl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C.
• 11:00-11:30: Yun-Sheng Chang (MIT): Verifying a high-performance distributed transaction system using partially consistent replication [abstract]
  In this talk, I'll introduce a high-performance distributed transaction system that we built and formally verified. The system uses sharding for scalability, replication within each shard for fault tolerance, and several performance optimizations -- including a new replication protocol called partially-consistent replication (PCR) -- to achieve single round-trip commit latency. Our evaluation results show that its performance matches or exceeds that of TAPIR, a highly optimized, unverified research system with a similar design. Moreover, the system has a simple, linearizable specification identical to that of a single-node transaction system, abstracting away implementation details such as crash recovery, multi-versioning, replication, sharding, and coordinator recovery. This talk is based on joint work with Joseph Tassarotti (NYU), Frans Kaashoek, and Nickolai Zeldovich.
• 11:30-12:00: Simon Oddershede Gregersen (New York University): Logical relations for formally verified authenticated data structures [abstract]
  Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. In this work, we give a formal proof of security and correctness for a library that generates authenticated versions of data structures automatically. The proof is based on a new relational separation logic for reasoning about programs that use collision-resistant cryptographic hash functions. This logic provides a basis for constructing two semantic models of a type system, which are used to justify how the library makes use of type abstraction to enforce security and correctness. Using these models, we also prove the correctness of several optimizations to the library and then show how optimized, hand-written implementations of authenticated data structures can be soundly linked with automatically generated code.
• 12:00-14:00: Lunch at FIAP
• 14:00-14:30: Yusuke Matsushita (Kyoto University): Nola: later-free ghost state for verifying termination in Iris [abstract]
  Separation logic (SL) has recently evolved at an exciting pace, opening the way to more complex goals, notably soundness proof of Rust's ownership type system and functional verification of Rust programs. In this paper, we address verification of termination in the presence of advanced features, especially Rust's ownership types. Perhaps surprisingly, this goal cannot be achieved by a simple application of existing studies that dealt only with safety properties. For high-level reasoning about advanced shared mutable state as used in Rust, they used higher-order ghost state (i.e., logical state that depends on SL assertions), but in a way that depends on the later modality, a fundamental obstacle to verifying termination. To solve this situation, we propose a novel general framework, Nola, which achieves later-free higher-order ghost state. Even in the presence of advanced features such as invariants and borrows, Nola enables natural termination verification, allowing arbitrary induction in the meta-logic. Its key idea is to parameterize higher-order ghost state, generalizing and subsuming the existing approach. Nola is fully mechanized in Rocq as a library of Iris. Moreover, to demonstrate the power of Nola, we develop a prototype of RustHalt, the first semantic and mechanized foundation for total correctness verification of Rust programs.
• 14:30-15:00: Egor Namakonov (Aarhus University): Lawyer: obligations-based reasoning for modular termination verification [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 higher-order reasoning, 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 higher-order liveness-aware specifications of modules.
• 15:30-18:00: Excursion to the Jardin des Plantes and Grande Galerie de l'Evolution
• 19:00-22:00: Banquet at Les Belles Plantes

Tuesday (3 June)

• 08:30-09:00: Coffee
• 09:00-10:00: Invited talk: Travis Hance (MPI-SWS): Leaf: A composable theory of shared resources as a basis for efficient systems verification [abstract]
  Recently, work in automated systems verification has demonstrated the utility of a formalism called a "storage protocol", used to formalize and verify concurrent permission protocols such as those found in bespoke lock implementations, concurrent message-passing, and memory allocation. One such work, using the Rust verification framework, Verus, is able to employ storage protocols efficiently because of nontrivial interactions with Rust's type system. In this talk, I will discuss the significance of these interactions and their formal underpinnings. The formal underpinnings use the Iris library, _Leaf_. Though the original Leaf paper [1] introduces storage protocols, it does not handle these type system interactions. I will discuss the recent evolution of Leaf that allows us to handle these interactions, simplifying its "core logic". In particular, I will discuss the novel _compositionality_ properties of Leaf that allow us to verify the soundness of these interactions in a modular way. [1] "Leaf: Modularity for Temporary Sharing in Separation Logic", Travis Hance, Jon Howell, Oded Padon, Bryan Parno (OOPSLA 2023).
• 10:00-10:30: Coffee
• 10:30-11:00: Lennard Gäher (MPI-SWS): RefinedRust: high-assurance verification of Rust programs [abstract]
  RefinedRust is a verification tool for Rust with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. It is based on a refinement type system proven sound in the Rocq prover against a RustBelt-based model. RefinedRust translates Rust code (with user annotations) into a formal model of Rust's execution embedded in Rocq, and then checks its adherence to the RefinedRust type system using separation logic automation in Rocq. All proofs generated by RefinedRust are checked by the Rocq prover (i.e., foundational), and consequently the automation and type system do not have to be trusted. The semantic model of RefinedRust's type system crucially relies on the advanced features of Iris, most importantly higher-order ghost state and later credits, with later credits enabling us to layer higher-order ghost state abstractions and replace a previous later hack used in RustBelt. In ongoing work, we use RefinedRust to verify core components of the ACE security monitor of IBM Research which provides a trusted execution environment (TEE). Low-level systems code like the ACE security monitor (which includes unsafe code in its core) are particularly interesting targets for foundational verification with RefinedRust: The properties we aim to verify are rich and security-critical, and the program code relies on low-level details of the Rust semantics and hardware. As part of this work, we are equipping RefinedRust to model and handle larger parts of the Rust language, like traits and closures.
• 11:00-11:30: Anton Lorenzen (University of Edinburgh): The Functional Essence of Imperative Binary Search Trees [abstract]
  Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, while an equivalent functional version might repeatedly allocate fresh nodes in memory. Based on the PLDI paper of the same name, this talk shows how imperative insertion algorithms for move-to-root, splay, and zip trees can be proven correct from a functional specification using Iris. While functional top-down algorithms usually involve non-tail calls, these can be removed using either a tail-modulo-cons transformation or destination-passing-style. In our paper, we introduce first-class constructor contexts to encapsulate destinations in a functional interface and use them to reformulate the functional algorithms. Constructor contexts can be modelled by list segments which allows us to show that the functional version corresponds closely to the imperative pseudo-code presented in the original papers; with most of the reasoning steps automatically handled by Diaframe.
• 11:30-12:00: Robbert Krebbers (Radboud University Nijmegen): An Inductive command for least fixpoints in Iris implemented using Rocq-Elpi [abstract]
  Inductive predicates play a key role in program verification using separation logic. There are many methods for defining such predicates, which all have different conditions and thus support different classes of predicates. The most common methods are: (1) through a structurally-recursive definition (commonly used to define representation predicates for the verification of data structures), and (2) through step-indexing (commonly used to give a semantics of Hoare triples). A lesser-known method is to define such inductive predicates _internally_ through a (least or greatest) fixpoint of a monotone function, as done in the the fixpoint_mono library in Iris. In this talk I will show that these fixpoints are useful to define representation predicates where the mathematical and in-memory data structures do not correspond, and that these fixpoints can be used to define Hoare triples and weakest preconditions for _total_ program correctness in Iris (a contribution by me from 2017 that has never appeared in a published paper). I will present a prototype command (akin to Rocq's Inductive) to generate the least fixpoint and its reasoning principles (constructors and induction principles) from a high-level specification. This command is implemented using the Rocq-Elpi language for meta programming. I will conclude the talk with some lessons learned and questions about integrating command/tactics written in Rocq-Elpi in the Iris Proof Mode. This is joint work with Luko van der Maas and Enrico Tassi.
• 12:00-14:00: Lunch at FIAP
• 14:00-14:30: Max Vistrup (ETHZ): HeapLang 2.0 [abstract]
  We show how to build up Heap Lang (among other languages) and its associated program logic as a composition of language extensions to a base lambda calculus. We hope that this will pave the way for easier experimentation with semantics and logic, such as trying out new memory models.
• 14:30-15:00: Clément Allain (Inria Paris): Zoo: a framework for the verification of concurrent OCaml 5 programs using separation logic [abstract]
  The release of OCaml 5, which introduced parallelism into the language, drove the need for safe and efficient concurrent data structures. New libraries like Saturn aim at addressing this need. From the perspective of formal verification, this is an opportunity to apply and further state-of-the-art techniques to provide stronger guarantees. We present a framework for verifying fine-grained concurrent OCaml 5 algorithms. Following a pragmatic approach, we support a limited but sufficient fragment of the language whose semantics has been carefully formalized to faithfully express such algorithms. Source programs are translated to a deeply-embedded language living inside Rocq where they can be specified and verified using the Iris concurrent separation logic.
• 15:00-16:00: Coffee
• 16:00-16:30: Remy Seassau (Inria Paris): Osiris: formal semantics and program logics for OCaml [abstract]
  OCaml is a mature, multi-paradigm, high-level programming language with a longstanding academic presence. With the advent of multicore OCaml came parallelism and concurrency, modernizing the language and leaving us with a pressing question: can we formalize it, and can we scale an instance of Iris up to it? We present OLang, a nontrivial fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, concurrency (WIP) and effect handlers. We show how to define the dynamic semantics of a realistic language as a monadic interpreter running atop a custom monad where computations are internally represented as trees of operations and effects are interpreted with a small-step semantics. We define two program logics for OLang: a stateless Hoare Logic allows reasoning about so-called pure programs, and an Iris-based Separation Logic allows reasoning about arbitrary programs.
• 16:30-17:00: Isaac van Bakel (ETHZ): Experience report: mechanising a frontend program logic with translational semantics [abstract]
  Automated verifiers often have specialised reasoning for features of their "frontend" source language(s), enabling both more expressivity in specifications and better coverage of real-world programs. Ensuring these reasoning principles are sound is tricky, but also vital to any verification result. However, instantiating Iris with a full-blown semantics for a source language can be a heavyweight obstacle to full mechanisation. I'll present my experience in using HeapLang as the target of a translational semantics for a core language showcasing some real-world features. This core language comes with reasoning principles used by real automated verifiers, and I'll describe how we proved these sound in Iris. I'll also talk about the encoding techniques we used for both program and logic translations.
• 17:00-17:30: Maxime Legoupil (Aarhus University): Iris-Wasm: formally establishing a robust and modular program logic for WebAssembly and its proposed extensions [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.

Wednesday (4 June)

• 08:30-09:00: Coffee
• 09:00-09:30: Thomas Somers (Radboud University Nijmegen): Verified lock-free session channels with linking [abstract]
  Type systems and program logics based on session types provide powerful high-level reasoning principles for message-passing concurrency. Modern versions employ bidirectional session channels that (1) are asynchronous so that send operations do not block, (2) have buffers in both directions so that both parties can send messages in parallel, and (3) feature a link operation (also called forward) to concisely write programs in process style. These features complicate a low-level lock-free implementation of channels and therefore increase the gap between the meta theory of prior work -- which is verified w.r.t. a high-level semantics of channels (e.g., pi-calculus) -- and the code that runs on an actual computer. We address this problem by verifying a low- level lock-free implementation of session channels w.r.t. a high-level specification based on session types. We carry out our verification in a layered manner by employing the Iris framework for concurrent separation logic. We start with an abstract specification of (unidirectional) queues -- of which we provide a linked-list and array-segment based implementation -- and gradually build up to session channels with all of the aforementioned features. To make a layered verification possible we develop two logical abstractions -- queues with ghost linking and pairing invariants -- to reason about the atomicity and changing endpoints due to linking, respectively. All our results are mechanized in the Coq proof assistant.
• 09:30-10:00: Bart Jacobs (KU Leuven): A program logic for XC20 grounded relaxed memory consistency [abstract]
  We propose an approach for verifying safety properties of programs that use relaxed-consistency atomic memory accesses, such as Rust's Atomic Reference Counting (ARC) implementation, against the recently proposed re-execution-based XMM memory model that, in contrast to earlier models used as a basis for verification, allows program-order-reads-from cycles (such as the Load Buffering litmus test) but rules out Out-Of-Thin-Air behaviors. Our approach is to define an interleaving operational semantics for a version of the programming language instrumented with begin_atomic operations that define a state transition system (STS) for each atomically accessed location, and treating atomic accesses as nondeterministically yielding any result allowed by the STS. We use the grounding guarantees provided by XMM to ensure all accesses are allowed by the STS. We then apply any logic for programs with an interleaving semantics, such as Iris. We have used the approach to verify ARC.
• 10:00-10:30: Coffee
• 10:30-11:00: Thomas Somers (Radboud University Nijmegen): Unifying Time Tracking for Multiple Later Elimination in Iris (WIP) [abstract]
  Recent Iris-based projects -- including Actris, RefinedRust, and Perennial -- rely on generating multiple later credits or eliminating multiple laters in a single program step. This number of generations and eliminations is tied to the number of prior program steps. In the current Iris implementation, the tracking of these steps and the dividing of later credits has been left to each specific instantiation of Iris. As a result, different Iris instances use different time-tracking methods (e.g., additive time receipts), and users of an instance are constrained by its chosen method. For example, in Linking Actris, we had to use the lower-bound step tracking provided by HeapLang, even though the additive time receipts provided by RefinedRust would have enabled cleaner specifications. We propose a unifying approach for later credit generation and later elimination by introducing a new step modality. This modality captures the later elimination rules of existing Iris instances as well as interactions between the different types of time receipts. It serves as a foundational building block for the weakest-precondition in Iris, enabling reasoning about multiple later eliminations across various Iris instances.
• 11:00-11:30: Simcha van Collem (Radboud University Nijmegen): Exceptional refinements: a separation logic for compositionally proving refinements of programs with exceptions [abstract]
  Proving contextual refinements directly is widely acknowledged to be hard. Additionally, contextual refinements are not compositional. The lack of compositionality is especially problematic in languages with exceptions, when one wants to compare throwing and non-throwing code. In prior work, the logical approach has been developed as a solution to these problems, particularly for rich languages with features such as concurrency and higher-order state. In this work, we extend the logical approach by also adding support for languages with exceptions. We achieve this by constructing a relational program logic, which has compositional reasoning rules and enables reasoning about concurrent, stateful programs with exceptions. The key idea of this program logic is that we generalize the type of postconditions, to reason about exceptions, improve compositionality, and have elegant rules to reason about concurrent programs. We formalize our work in Rocq using Iris.
• 11:30-12:00: Youngju Song (MPI-SWS): Refinement composition logic [abstract]
  One successful approach to verifying programs is refinement, where one establishes that the implementation (e.g., in C) behaves as specified in its mathematical specification. In this approach, the end result (a whole implementation refines a whole specification) is often established via composing multiple "small" refinements. In this paper, we focus on the task of composing refinements. Our key observation is a novel correspondence between the task of composing refinements and the task of proving entailments in modern separation logic. This correspondence is useful. First, it unlocks tools and abstract constructs developed for separation logic, greatly streamlining the composition proof. Second, it uncovers a fundamentally new verification strategy. We address the key challenge in establishing the correspondence with a novel use of angelic non-determinism. Guided by the correspondence, we develop RCL (Refinement Composition Logic), a logic dedicated to composing refinements. All our results are formalized in Coq.
• 12:00-14:00: Lunch at FIAP
• 14:00-15:00: Gil Hur (Seoul National University): CRIS: the power of imagination in specification and verification [abstract]
  Just as imaginary numbers extend real numbers and simplify certain mathematical proofs, we introduce the concept of imaginary specifications to enhance program verification. In mathematics, imaginary numbers enable expressing intermediate steps that cannot be captured using real numbers alone, offering natural proof decomposition that reduces complex proofs into simpler, more manageable steps. Similarly, our work introduces imaginary specifications in program verification through CRIS (Contextual Refinement with Imaginary Specification), our novel verification tool. CRIS with imaginary specifications provides a unified framework to inherently marry two fundamental approaches to program verification: separation logic with pre/post conditions as specifications, and program refinement with abstract programs as specifications. This unification not only enables proof simplification via proof decomposition but also enables elegant expression of hard-to-express properties, such as separation logic conditions involving IO events and logical atomicity -- properties that traditionally require intricate mechanisms or are difficult to specify. The CRIS framework uses the IPM proof mode and the Iris resource algebra libraries, supporting most of the key features of Iris.
• 15:00-16:00: Coffee
• 16:00-16:30: Janine Lohse (MPI-SWS): Amaryllis: modular probabilistic reasoning with independence and conditioning [abstract]
  Probabilistic program logics can be used to reason about the distribution of program outputs, their probabilistic independence, or expected outcomes. The most general of these logics use a conditioning modality to facilitate a convenient form of case-by-case reasoning. A crucial law for reasoning with conditioning is the commuting rule between the conditioning modality and the weakest precondition, which is needed whenever a case distinction needs to be made before the program has terminated. However, justifying this law has proven to be challenging---thus, existing logics only support it in a restricted fashion, sacrificing either modularity or expressiveness. In this talk, we present Amaryllis, a probabilistic program logic that combines expressiveness and modularity with a general rule for commuting the weakest precondition and the conditioning modality. Amaryllis extends Iris with a conditioning modality and introduces the concept of a probabilistic-frame preserving update as the key to achieving the commuting rule. This novel concept of a probabilistic update modality additionally enables support for dynamic allocation, which was previously out of reach for probabilistic program logics with conditioning.
• 16:30-17:00: Kwing Hei Li (Aarhus University): Coneris: modular reasoning about error bounds for concurrent probabilistic programs [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 supports modular reasoning about error bounds for concurrent probabilistic modules.
• 17:00-17:30: Guillaume Bertholon (Inria Strasbourg): OptiTrust: Invariant-Preserving Source-to-Source Transformations [abstract]
  Producing a formally verified program is a very challenging, highly time-consuming task. Producing a high-performance code is another very challenging, highly time-consuming task. Could we produce code that is both high performance and formally verified, without losing sanity? To tackle this challenge, we developed OptiTrust, an interactive, invariant-preserving, source-source optimization framework. The user starts from an unoptimized code, accompanied with Separation Logic specifications as well as invariants justifying the correctness of the code. Optimizations are then introduced by means of a transformation script. Each line of this script indicates what program transformation to apply, and where in the code to apply it. Each transformation takes care of preserving the invariants. As a result, the final optimized code carries evidence of its correctness. In this talk, we will present a demo showing how to use OptiTrust for producing a highly optimized implementation of matrix-multiply with formal guarantees, and we will explain the key design choices and the novel ingredients involved.

Thursday (5 June) – Friday (6 June)

• Discussion groups and meetings organized by attendees.

Location

The workshop will take place at Inria, 48 rue Barrault, Paris, France (directions; map).

Once you enter the building, the Lions amphitheater is on your right, next to the entrance hall.

During the entire week (June 2-6), two meeting rooms, named Ada Lovelace (16 people) and Catherine Johnson (6 people) have been reserved for the participants of the workshop. They can be used by people who would like to meet or work privately. These rooms are located behind the coffee space, which itself is on the side of the Lions amphitheater.

On June 5 (morning only), we also have room Emmy Noether (30 people). On June 6, we have room Philippe Flajolet (50 people).

Practical information

Directions to Inria

• From Charles de Gaulle airport (CDG) or from Gare du Nord, take RER line B (headed South) until Denfert-Rochereau or Cité Universitaire.
• From Denfert-Rochereau, either walk 20 minutes to Inria (itinerary) or take metro line 6 (headed East, towards Nation) to Corvisart.
• From Cité Universitaire, walk 12 minutes to Inria (itinerary). As you exit the station, immediately enter Parc Montsouris, and cross the park, walking North-East.
• From Corvisart, walk 7 minutes to Inria (itinerary).
• From Orly airport (ORY), take metro line 14 until Olympiades.
• From Olympiades, take bus number 62 (headed West, towards Porte de Saint-Cloud) to Vergniaud. Once you exit the bus, turn the corner into rue Barrault (itinerary).

Food

Here are some places where you can find food near Inria.

Pastry, bread, and sandwiches:

• Laurent Duchêne, a high-end pastry shop, is only 5 minutes away, and well worth a visit, if only to buy a great croissant au chocolat or chausson aux pommes.
• Délice de Paris 13, 5 minutes away, is a typical boulangerie.
• Lorette, 10 minutes away, has organic bread and good pastry.

Drinks:

• Café Circus, 2 minutes away, is a typical Parisian café (coffee, tea, drinks).
• La Folie en Tête, 3 minutes away, is a nearby bar (drinks).
• Biérocratie, a beer cellar, sells a wide selection of beers (some chilled) (closed Monday).

Restaurants:

• Café Circus, a typical Parisian bar, serves lunch and dinner and offers a good quality/price ratio.
• Fabbrezza makes good pizza.
• La Bonne Heure is a tiny vegan/vegetarian place (making a reservation is highly recommended).
• Les Cailloux is an unsophisticated trattoria.
• Chez Gladines and Auberge Etchegorry serve hefty French Sud-Ouest cuisine.
• Lancetta is a true Italian place; somewhat high-end and expensive.
• Chez Nathalie serves French cuisine; somewhat high-end and expensive.
• Marso & Co serves French cuisine; leans on the chic and expensive side.

Organizers

• François Pottier (Inria, Paris, France)
• Jacques-Henri Jourdan (CNRS, France)