LogSem Seminar talks in 2024

30-09-2024: Introduction to Guarded Interaction Trees.

Speaker: Sergei Stepanenko, Aarhus University

Time: 13:00-14:00

Location: Ada-333

Abstract: Abstract: Despite significant progress, representing and reasoning about programming languages in proof assistants like Coq remains a major challenge. The design space is broad, and many approaches have been explored. One notable recent development is the introduction of Interaction Trees (ITrees), a novel approach aimed at simplifying the representation and reasoning of potentially non-terminating first-order programs with side effects in Coq.

ITrees provide an elegant abstraction for denotational semantics, allowing one to bypass the syntactic complexities commonly encountered in operational-styled semantics. Specifically, ITrees facilitate the modular representation and reasoning of various effects and their combinations. Applications have shown that ITrees work particularly well for reasoning about first-order programs with first-order effects.

However, a key limitation of ITrees is their inability to support higher-order computations and higher-order effects directly. To address this, Guarded Interaction Trees (GITrees) were introduced. GITrees are an alternative approach based on ideas established by the ITree framework, which offers a formalized structure that accommodates higher-order computations and higher-order effects within Coq.

In this informal talk, we will explore the motivation behind Guarded Interaction Trees, introduce the framework, and showcase its applications.

07-10-2024: Osiris: an Iris-based program logic for OCaml.

Speaker: Arnaud Daby-Seesaram, Aarhus University

Time: 13:00-14:00

Location: Nygaard-298

Abstract: Osiris is a project that aims to help OCaml developers verify their code using Separation Logic. Iris has been instantiated with several OCaml-like languages. Yet, none of these instances allow to reason on real-life OCaml programs. Osiris attempts to fix this. The project is still young, so it only supports a subset of the features of the OCaml language at the moment. At the end of my internship¹, the supported subset notably included modules, (mutually) recursive functions, ADTs and deep-pattern matching with bindings. A long-term goal is to add more language features² while keeping the semantics and program reasoning as simple as possible.

Usual techniques for instantiating Iris do not scale well: writing a small-step semantics of a large non-deterministic language such as OCaml is laborious. In this talk, I will explain how we have defined our program logic so that the semantics remains simple (and is easy to extend with new language features). I will also present a methodology to verify a concrete OCaml file using Osiris, and discuss limitations of Osiris (as at August 2023).

¹: My internship ended in August 2023.

²: Features have been added since I left. For example, OCaml5 effect handlers are now supported (built on previous work, Hazel).

10-10-2024: Type Systems for Numerical Error Analysis.

Speaker: Justin Hsu, Cornell University

Time: 11:00-12:00

Location: Nygaard-295

Abstract: Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity.

Today, I’ll talk about some of our recent work developing two type systems for statically bounding the roundoff error. The first type system, NumFuzz, is a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Subject to certain restrictions, our type inference procedure derives sound relative error bounds for programs that are several orders of magnitude larger than previously possible, while deriving relative error bounds that are several orders of magnitude more precise than prior work.

The second type system, Bean, is a first-order language for bounding backward error. Like NumFuzz, Bean is based on a linear coeffect type system, but it features a novel semantics based on a category of lenses on metric spaces, which we call backward error lenses. Bean is the first work to soundly reason about backward error in numerical programs.

Joint work with Ariel Kellison (Cornell).

14-10-2024: Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly.

Speaker: Maxime Robert Sébastien Legoupil, Aarhus University

Time: 13:00-14:00

Location: Ada-333

Abstract: WebAssembly offers coarse-grained encapsulation guarantees via its module system, but does not support fine-grained sharing of its linear memory. MSWasm is a recent proposal which extends WebAssembly with fine-grained memory sharing via handles, a type of capability that guarantees spatial and temporal safety, and thus enables an expressive yet safe style of programming with flexible sharing. In this paper, we formally validate the pen-and-paper design of MSWasm. To do so, we first define MSWasmCert, a mechanisation of MSWasm that makes it a fully-defined, conservative extension of WebAssembly 1.0, including the module system. We then develop Iris-MSWasm, a foundational reasoning framework for MSWasm composed of a separation logic to reason about known code, and a logical relation to reason about unknown, potentially adversarial code. Iris-MSWasm thereby makes explicit a key aspect of the implicit universal contract of MSWasm: robust capability safety. We apply Iris-MSWasm to reason about key use cases of handles, in which the effect of calling an unknown function is bounded by robust capability safety. Iris-MSWasm thus works as a framework to prove complex security properties of MSWasm programs, and provides a foundation to evaluate the language-level guarantees of MSWasm.

21-10-2024: How to deal with rejections – Separation logics for probability.

Speaker: Kwing Hei Li, Aarhus University

Time: 13:00-14:00

Location: Ada-026

Abstract: Randomess acts as the sole backbone for some of the most crucial software ever written. From the world of security, the use of entropy obscures private data and allows encryption, authentication, and other basic cryptographic operations between parties. From the algorithms perspective, probabilistic data structures can often be more efficient alternatives than the non-randomized counterparts, especially when approximate solutions are sufficient. It is not surprising that though randomness in programs are useful, it also makes the reasoning of those programs more challenging.

In this INFORMAL talk, we explore how one leverages separation logics to reason about probabilistic programs, and observe how various aspects of probability can be encoded as separation logic resources. Throughout the presentation, we specifically focus on verifying properties of rejection samplers, a common pattern found in probabilistic programs. Specifically, we first use Tachis to reason about its expected runtime cost, and then, Eris (and Eris_t) to prove strict error bounds of its behavior.

28-10-2024: The state of the Creusot verifier

Speaker: Armaël Guéneau, INRIA

Time: 13:00-15:00

Location: Ada-333

Abstract: I will give (to the best of my abilities) an informal overview of the state of the Creusot deductive verification tool for Rust, developed at LMF. Creusot allows annotating Rust programs with specifications and formally verify their correctness. I will explain how Creusot manages to achieve high automation by offloading lightweight proof obligation to SMT solvers, while providing extensive support for idiomatic Rust features such as borrows, traits, iterators and closures. I will then talk about exciting ongoing work on adding “linear ghost code” to Creusot, opening the way for separation-logic-like reasoning in Creusot.

(Most of the work I will be presenting is not mine, but my colleagues': Xavier Denis, Arnaud Golfouse, Jacques-Henri Jourdan)

04-11-2024: Synchronous Programming for Kids: A Manifesto

Speaker: Jean Pichon-Pharabod, Aarhus University

Time: 13:00-14:00

Location: Ada-333

Abstract: Primary school age children find developing games and interactive animations very motivating, and this has been successfully leveraged by several educational programming environments. However, most of these environments, like Scratch and Microsoft MakeCode, are fundamentally based on imperative, Pascal-style programming languages with ad-hoc support for concurrency and events. We argue that this style of programming language, and the burden of encoding state machines that it imposes, does not match the children’s intuitions, and is discouraging. Instead, we propose re-founding these tools around synchronous programming languages like Esterel, which, by being centred around the concepts of concurrency, signalling, and preemption, match the children’s intuitions. We provide a prototype implementation, and argue how using such a programming language would enable schoolchildren to express their intuitions more directly.

18-11-2024: Formally Specifying ABIs using Realistic Realizability

Speaker: Amal Ahmed, Northeastern University

Time: 13:00-14:00

Location: Ada-333

Abstract: The Application Binary Interface (ABI) for a language specifies the interoperability rules for each of its target platforms, including properties such as data layout and calling conventions, such that compliance with the rules will ensure ``safe'' execution and perhaps provide certain guarantees about resource usage. These rules are relied upon by compilers for that language and others, libraries, and foreign-function interfaces. Unfortunately, ABIs are typically specified in prose and, while type systems for source languages have grown richer over time, ABIs have largely remained the same, lacking analogous advances in expressivity and safety guarantees.

I’ll outline a vision for richer, semantic ABIs that would facilitate safer interoperability and library integrations, supported by a methodology for formally specifying ABIs using realizability models. These semantic ABIs relate abstract, high-level types to unwieldy, but well-behaved, low-level code. We demonstrate the approach with a case study that formalizes the ABI of a functional source language in terms of a reference-counting implementation in a C-like target language. An important contribution is our reference-counting realizability model which uses a novel extension to separation logic that captures how each reference owns a share to the reference-counted resource. I’ll discuss how different practically-motivated ABI design decisions can be interpreted via a semantic ABI and present the first formalization of a Swift-style ABI with library evolution

25-11-2024: Reasoning about concurrency with graphs instead of heaps in Iris

Speaker: Zongyuan Liu, Aarhus University

Time: 13:00-14:00

Location: Ada-333

Abstract: A common way to model shared-memory concurrency of a programming language is through small-step operational semantics that specify how threads interact with a shared, mutable heap representing memory. This form of semantics is also the typical foundation for Iris-based logics.

In this informal talk, I will explain how to construct Iris logics based on a different shape of semantics, where memory is represented as an immutable graph. I will demonstrate this approach by developing a simple logic for sequential consistency and showing how to prove its adequacy theorem.

Finally, I will touch on how this graph-based approach can be used to reasoning about relaxed memory concurrency, where straightforward operational semantics are often unavailable.

02-12-2024: Correctness of Time-forward Processing Algorithms

Speaker: Steffan Christ Sølvsten, Aarhus University

Time: 14:00-15:00

Location: Nygaard-295

Abstract: During the past five years, we’ve been developing yet another BDD package, Adiar. What sets this one apart is its non-recursive algorithms which enables efficient computation on BDDs larger than the RAM of your machine - this potentially pushes the limits of symbolic model checking.

Yet, Adiar is implemented in C++ and its correctness has only been “proven” by means of a lot of unit and integration testing. In this talk, I’ll try to sketch how these algorithms (1) can be written as pure and tail-recursive functions that inherently are I/O-efficient and (2) can be proven correct.

09-12-2024: Compositional Verification of Composite Byzantine Protocols

Speaker: Ilya Sergey, National University of Singapore

Time: 13:00-14:00

Location: Ada-333

Abstract: Byzantine Fault-Tolerant (BFT) protocols are known to be challenging to design due to the complexity of their execution scenarios in the presence of arbitrary communication faults and potentially adversarial behaviour of the participants. To address this challenge, on the one hand, several approaches have been developed recently for computer-aided formal verification of the desired correctness properties, both safety and liveness, of standalone BFT protocols. On the other hand, the distributed computing community has made attempts to reduce the conceptual complexity of constructing new such protocols by showing how to assemble them from simpler “building blocks”. No methodology to date combines these two approaches for foundational verification of arbitrary BFT protocols.

We present Bythos, the first foundational framework for compositional mechanised verification of both safety and liveness of composite BFT protocols. Bythos is implemented on top of the Coq proof assistant and uses Coq’s higher-order logic to reuse proofs of common facts about knowledge and trust in BFT protocols. It allows for compact liveness specifications in the style of TLA+, and their proofs using an embedding of TLA into Coq. Most importantly, Bythos provides a family of higher-order definitions that allow for building composite BFT protocols from simpler ones, with their correctness proofs derived, in a way that matches the intuition of the protocol designers. Protocols verified in Bythos are executable and can serve as reference implementations. We showcase Bythos by proving in it safety and liveness properties of three basic BFT protocols: Reliable Broadcast, Provable Broadcast, and the recently proposed Accountable Byzantine Confirmer, as well as a number of protocols constructed by composing them.

Bio: Ilya Sergey is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. Ilya got his PhD in Computer Science at KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to becoming an academic, he worked as a software developer at JetBrains. Ilya does research in programming language design and implementation, distributed systems, software verification, and program synthesis. He is a recipient of several distinguished paper awards at POPL and PLDI, the 2019 Dahl-Nygaard Junior Prize, Yale-NUS Distinguished Researcher award, and academic research awards from Google, Facebook, and Amazon.

10-12-2024: Mechanised Hypersafety Proofs about Structured Data

Speaker: Ilya Sergey, National University of Singapore

Time: 15:00-16:00

Location: Ada-333

Abstract: Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of manipulations with such structured data is challenging, as they are often composed of multiple loops with non-trivial invariants.

In this work, we observe that specifications for structured data manipulations can be phrased as hypersafety properties, i.e., predicates that relate traces of programs. To turn this observation into an effective verification methodology, we developed the Logic for Graceful Tensor Manipulation (LGTM), a new Hoare-style relational separation logic for specifying and verifying computations over structured data. The key enabling idea of LGTM is that of parametrised hypersafety specifications that allow the number of the program components to depend on the program variables. We implemented LGTM as a foundational embedding into Coq, mechanising its rules, meta-theory, and the proof of soundness. Furthermore, we developed a library of domain-specific tactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts that enjoy a high degree of reuse. We argue for the effectiveness of relational reasoning about structured data in LGTM by specifying and mechanically proving correctness of 13 case studies including computations on compressed arrays and efficient operations over multiple kinds of sparse tensors.