Arrival, Check-in, Coffee
Welcome
Complexity class of JavaScript regex matching, in Rocq
Victor Deng, EPFLAbstract
JavaScript regexes are widely used in JavaScript programs, but the complexity class of the JavaScript regex matching problem has not yet been well-understood. We present ongoing work on proving several complexity class results for JavaScript regex matching: JavaScript regex matching is PSPACE-hard and OptP-hard, even without negative lookarounds; JavaScript regex matching without forced quantifiers is PSPACE-complete; JavaScript regex matching without forced quantifiers and without lookarounds is OptP-complete. The proofs are mechanized in the Rocq proof assistant.
Precise Reasoning about Container-Internal Pointers with Logical Pinning 🔗
Yawen Guan, EPFLAbstract
Most separation logics hide 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.
We present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Our model generalizes the magic-wand operator for representing partial data structures, making it easy to write and prove precise specifications, including pointer-stability properties. Because it only changes the way representation predicates and specifications are written, our approach is compatible with most separation logic variants.
We demonstrate the practicality of logical pinning by verifying small but representative pointer-manipulating programs, and deriving more precise versions of common container specifications. In doing so, we show that our approach 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.
CHC-Based Reachability Analysis via Cycle Summarization 🔗
Konstantin Britikov, University of LuganoAbstract
Modern reachability analysis techniques are highly effective when applied to software safety verification. However, they still struggle with certain classes of problems, particularly the verification of programs with complex control flow and deep nested loops. In this paper, we introduce Cycle Summarization-based Reachability Analysis (CSRA), a new Constrained Horn Clause (CHC) based approach for reachability analysis of nested-loop software. Our technique relies on the generation and refinement of cycle summaries within the CHC system. CSRA analyzes cycles in a modular manner, constructing summaries and cycle unrollings. Cycle summaries in our approach are used both to prove safety and detect potential safety violations. This enables more efficient exploration of nested loops. The prototype of CSRA is implemented within the Golem CHC solver. An empirical comparison with other reachability analysis techniques demonstrates that our approach is highly competitive in both proving safety and constructing counterexamples.
A Refinement Methodology for Distributed Programs in Rust
Aurea Bílá, ETH ZurichE-Graphs for Property-Based Testing
David Spielmann, University of St. GallenAbstract
E-graphs are established in verification and automated reasoning as a mechanism for efficiently deciding equivalence relations between expressions. More recently, multiple extensions have been proposed to instead extract equivalent expressions. In this talk, I present a novel application of these techniques to automated test input generation. I will discuss how e-graphs can be used to generate diverse sets of equivalent inputs for validating software systems.
Group Photo
Lunch
Functional Programming for the (hopefully) Hungry Masses!
Farhad Mehta, OSTInteractive Proofs for Self-Stabilizing Algorithms using PADEC
Karine Altisen, Université de GenèveAbstract
PADEC is a framework to build machine-checked proofs of self-stabilizing algorithms using the Coq/Rocq proof assistant. The framework includes the definition of the computational model, tools for time complexity and composition of algorithms, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions. This talk gives an overview of the framework along with recent developments.
Programming Without References 🔗
Dimi Racordon, HES-SO Valais-WallisAbstract
Taming the unintended consequences of shared mutable state has been a decades-long quest in both industry and academia. While programming languages like Rust and more recent efforts like Scala's capture checking have demonstrated the benefits of this effort, balancing the expressiveness and complexity costs of alias tracking mechanisms remains a timely issue.
For a little more than five years, I have been exploring a different direction: programming without references. It turns out that this restriction yields a neat discipline, mutable value semantics, which is expressive enough to write efficient in-place algorithms, offers many of the benefits of pure functional programming, and does not require sophisticated typing features.
In this talk, I will present Hylo, a programming language for systems programming that embraces mutable value semantics. After a quick review of key features, I will show how to design safe and efficient data structures and algorithms without resorting to references.
Letting go of data privately with budgeted declassification
Ali Mohammadpur-fard, Università della Svizzera ItalianaAbstract
Collaborative environments often need to share sensitive data across different trust levels, yet existing tools either ignore security hierarchies (treating data as simply "private" or "public") or treat release as all-or-nothing with no way to control how much is leaked. We introduce a language-level mechanism that unites differential privacy with information-flow control, making declassification a first-class, type-checked feature governed by privacy budgets. This allows the enforcement of a novel "noninterference up to ε" property, ensuring bounded leakage across security boundaries. A prototype shows that programs using this approach are significantly shorter than ad-hoc alternatives while achieving higher accuracy with equivalent budgets.
Probabilistic Model Checking of Quantum Networks 🔗
Lorenzo La Corte, Università della Svizzera ItalianaAbstract
Quantum networks enable capabilities that are impossible using classical information alone. They connect quantum-capable nodes by distributing entangled pairs of qubits, which serve as a fundamental resource for communication. To distribute entanglement, quantum network protocols rely on inherently probabilistic operations acting on short-lived resources. In addition, resource contention may arise when operations execute in parallel, introducing nondeterministic behavior. This makes quantitative analysis essential for the design and optimization of quantum networking protocols. This talk presents ongoing work on the formal specification and analysis of quantum networks using probabilistic model checking techniques. We show how entanglement distribution protocols can be modeled as Markov decision processes, capturing both probabilistic effects and nondeterminism arising from scheduling and resource contention. We then apply quantitative methods to compute expected costs, cost-bounded reachability probabilities, and extremal cost distributions. Together, these results provide a systematic framework for reasoning about performance guarantees and trade-offs in quantum network protocols.
Verified Composable CRDTs
Alexander Städing, University of St. GallenCoffee Break
Advancing Formal Verification at CERN: Updates on PLCverif and Neural Network Verification Challenges
Xaver Fink, CERN & RWTH Aachen UniversityAbstract
The CERN BE-ICS group is integrating formal methods into the engineering and validation of safety-relevant control software for particle accelerators. This talk gives an update on our Programmable Logic Controller (PLC) and Neural Network (NN) verification activities, with an emphasis on work-in-progress topics where we actively seek discussion and collaboration.
On the PLC side, we report on the ongoing consolidation of the open-source PLCverif framework. We also share recent experience from analyzing CERN’s UNICOS baseline objects (a widely reused PLC framework component), where PLCverif uncovered implementation inconsistencies and specification mismatches. Potential future directions are (i) stronger model checking k-induction proofs via LLM-supported invariant synthesis, (ii) Model-Based software engineering.
On the NN side, we outline three verification challenges emerging from CERN control applications: (i) sequence-level robustness for time-series classifiers used in beam instrumentation, (ii) verification of reinforcement-learning policies for beam alignment under uncertainty, and (iii) planned verification of NN approximations of MPC (e.g., cooling and energy systems).
Agentic Proof Automation: A Case Study 🔗
Yichen Xu, EPFLAbstract
Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language models (LLMs) create new opportunities for proof automation: modern LLMs not only generate proof scripts, but also support agentic behavior, exploring codebases and iteratively refining their outputs against prover feedback. These advances enable an emerging scheme where LLM-based agents undertake most proof engineering under human guidance. Humans provide mathematical insight (definitions, theorems, proof strategies); agents handle the mechanical work of proof development. We call this scheme agentic proof automation. We present this scheme through a case study: mechanizing the semantic type soundness of a sophisticated formal system, System Capless, in Lean 4, comprising over 14,000 lines of code. Using off-the-shelf LLM agents with a single lightweight proof-checking tool, the agents completed 189 proof engineering tasks with an 87% success rate, only 16% requiring human intervention. The case study demonstrates that agents are capable proof engineers that substantially boost productivity, though they fall short in creative reasoning and still require human guidance in certain cases. We release an interactive explorer where readers can examine all agent interactions; the mechanization is open-sourced for experiments and extensions.
Space Explanations: Formal and General Explanations of NNs
Faezeh Labbaf, University of LuganoAbstract
Space Explanations are formal explanations for neural networks that give provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art. I will present the work in progress in our group on computing space explanations.
Utilising the PCG in Prusti
Jonas Fiala, ETH ZurichAbstract
Recent work on Place Capability Graphs (PCG) for Rust provides a complete model of Rust's type-checking results. In this talk, we will explain how Prusti now leverages this PCG model, which simplifies Prusti's implementation and allows it to support more complicated borrowing patterns.