Precise Reasoning about Container-Internal Pointers with Logical Pinning
Speaker: Yawen Guan
Yawen is a fourth-year PhD student at EPFL, Switzerland, advised by Prof. Clément Pit-Claudel. She works on program verification, with a focus on ensuring the correctness of low-level, efficient programs. Her current project targets systematic verification of mutable containers. She also has broader interests in software engineering, including proof visualization.
Abstract
Separation logic is the state-of-the-art approach to reason about mutable containers, which typically hides container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs. In this talk, I will present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Our approach is compatible with most separation logic variants, subsumes some well-known proof patterns, simplifies some complex proofs, and enables reasoning about program patterns not supported by traditional specifications. All of our results are mechanized in the Rocq proof assistant, using the CFML library.
Predictable & Interactive Proof Search
Speaker: Cassia Torczon
Cassia is a PhD student at the University of Pennsylvania, advised by Benjamin Pierce (University of Pennsylvania) and Harry Goldstein (University at Buffalo). Her work focuses on proof assistant usability, particularly how to leverage the interactive structure of theorem provers like Lean and Rocq to reduce friction in the theorem proving process.
Abstract
In this talk, I describe Hoverfly, a new user interface for interactive proof search. I'll start by presenting our motivating example: Palamedes, a tool for deductive synthesis of constrained random generators for property-based testing that we implemented using Lean's aesop proof search tactic. I'll describe some frustrations with proof search that we encountered while developing this tool, as well as our proposed solution: a user interface that exposes the underlying AND-OR tree behind proof search and allows the user to easily and predictably navigate it.
Expectation Credits: Resourceful expected value reasoning for higher-order probabilistic programs
Speaker: Markus de Medeiros
I am a third-year PhD student at New York University studying under Joseph Tassarotti. My research is focused on verification techniques for probabilistic programs, with applications to privacy and security.
Abstract
Several properties of probabilistic programs are related to expected values, such as error bounds, termination bounds, or the expected runtime cost. Verifying these properties can be challenging, and prior program logics designed to verify expected value properties suffer from compositionality issues in the presence of features such as higher-order functions and state. In this talk, I will discuss three program logics which address these compositionality issues by encoding expected values as resources in a separation logic.
Backwards Under-Approximation with (Separation) Incorrectness Logics
Speaker: Flavio Ascari
Flavio Ascari is a postdoctoral researcher at the University of Konstanz, Germany, where he has been working since 2025 on the deductive verification of probabilistic programs using (probabilistic) separation logic. He received his PhD from the University of Pisa, Italy, in 2025. During the PhD he focused on under-approximation program analysis for bug finding, initially from an abstract interpretation perspective and later through (separation) program logics. He has also worked on combining under- and over-approximation techniques via abstract interpretation and model checking (in a PDR/IC3-style). During his Bachelor's and Master's studies, he was supported by a full scholarship from the Scuola Normale Superiore di Pisa.
Abstract
Static analysis has traditionally been studied as an over-approximation technique to prove program correctness. In practice, however, many industrial-strength static analyzers are primarily used for bug finding. This dual view was brought to the forefront by Incorrectness Logic, which initiated a growing line of research on under-approximation techniques for identifying program errors.
In this talk, I describe my journey toward identifying sources of errors, that is, initial program states that lead to failures. This path led me to the study of backwards under-approximation analyses for heap-manipulating programs.
I first introduce Sufficient Incorrectness Logic, a backwards counterpart to O'Hearn's Incorrectness Logic, and discuss its underlying principles. I then show how these ideas can be lifted to Separation Sufficient Incorrectness Logic, enabling the analysis of heap-manipulating programs and opening the door to automated backwards reasoning. A naive application of this analysis, however, suffers from a combinatorial explosion in the number of explored program paths. To address this challenge, I present a proof strategy that combines a preliminary forward analysis, performed using "plain" Incorrectness Logic, with the backwards analysis. This forward step acts as a guide, restricting the backwards exploration to program paths that are guaranteed to succeed in identifying sources of errors.
Verifying Rust programs with Creusot
Speaker: Li-yao Xia
Li-yao Xia ([https://poisson.chat](https://poisson.chat)) is a research engineer at Laboratoire Méthodes Formelles, with a background in Haskell and Rocq.
Abstract
Rust is a low-level programming language that looks high-level thanks to a rich type system that guarantees memory safety with a strict ownership discipline. Creusot is a deductive verifier for Rust programs: users specify Rust functions using pre- and postconditions, and Creusot proves that functions satisfy those specifications. In this talk, I will give a tour of the tool and its core features, and show how we can reason about imperative programs with mutable references without separation logic.
Typing Strictness
Speaker: Daniel Sainati
Daniel Sainati is a 2nd year PhD Student in the PLClub at UPenn working with Benjamin Pierce and Stephanie Weirich on type systems and language design. Before starting his PhD, he worked in PL in industry at Meta and the Flow Foundation, and before that he completed his undergraduate and master's degrees at Cornell, advised by Adrian Sampson.
Abstract
Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. In this talk, I will give an overview of the existing definition of strictness, detail its shortcomings, and propose a new definition that refines it by describing variable usage more precisely. I will then outline two type systems that capture this new definition in both call-by-name and call-by-push-value settings, employing techniques from the literature on effect and coeffect systems. I'll give an overview of how these systems work, what we've proved about them, and what benefits we derive from our new definition of strictness.
Foundations of equality in dependent type theory
Speaker: Katie Casamento
I'm a PhD student and sometime-instructor at Portland State, usually lecturing on things like programming language theory, formal methods, and software maintenance. I finished my MS at Portland State in 2019, which included a thesis on verified typechecking in languages with complex scoping. Agda is my favorite puzzle game. In my recent free time I've been playing pinball and figuring out how to write music for the Game Boy.
Abstract
One of the most common beginner stumbling blocks in Agda is the seemingly chaotic behavior of the equality type constructor refl (short for "reflexivity"), which can sometimes make short work of otherwise long complex proofs but also somehow can't prove x + 0 = x. Rocq and Lean generally hide this level of detail from the programmer under the abstraction of a tactics language, but the same foundational weirdness about equality is down there in the language of proof terms, ready to strike if you get too close. Why is "reflexivity" so smart and so stupid at the same time? Let's talk about it!
We'll begin with definitional equality and the conversion typechecking rule for an explanation of how a typechecker "reasons" about equality internally. We'll explore how definitional equality interacts with dependent pattern-matching and in the process we'll discover that the standard propositional equality type (the one we like to prove things about) falls out of this interaction as a special case. Things will go pretty smoothly until we start asking too many questions about equality between functions, at which point we find ourselves in a kind of foundational crisis. We'll survey some ways to resolve this problem like importing the entire field of synthetic topology (homotopy type theory) or ignoring it really hard (proof erasure).
By the end of this talk you'll hopefully have a decent conceptual framework for understanding and debugging the errors that you get when working with equality proofs in a dependently-typed language. You'll also have some context for why some parts of the PL world are so interested in fancy new types of equality, although you might reasonably conclude that you don't need them yourself.