Volume
LIPIcs, Volume 372
40th European Conference on Object-Oriented Programming (ECOOP 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
Editors
Publication Details
- published at: 2026-06-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-423-9
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 372, ECOOP 2026, Complete Volume
Abstract
LIPIcs, Volume 372, ECOOP 2026, Complete Volume
Cite as
40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 1-914, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{krebbers_et_al:LIPIcs.ECOOP.2026,
title = {{LIPIcs, Volume 372, ECOOP 2026, Complete Volume}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {1--914},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026},
URN = {urn:nbn:de:0030-drops-267312},
doi = {10.4230/LIPIcs.ECOOP.2026},
annote = {Keywords: LIPIcs, Volume 372, ECOOP 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{krebbers_et_al:LIPIcs.ECOOP.2026.0,
author = {Krebbers, Robbert and Silva, Alexandra},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.0},
URN = {urn:nbn:de:0030-drops-267296},
doi = {10.4230/LIPIcs.ECOOP.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis
Abstract
Pointer analysis for Rust faces unique challenges arising from its ownership-based memory model and layered abstractions, which complicate how heap-allocated objects flow across functions. Existing k-limited callsite abstractions - designed for earlier languages - are both imprecise and inefficient on large Rust programs. We present Rceus, a Rust-oriented pointer-analysis technique that mitigates points-to set explosion and resource exhaustion caused by cross-function pointer conflation under deep heap encapsulation, a scalability bottleneck that conventional k-limiting cannot address.
Rceus performs a fast, coarse-grained pointer-flow pre-analysis to identify precision-critical functions and the essential callsites within their calling contexts. This selective context construction distinguishes parameter-derived flows while avoiding unnecessary expansion. As a result, Rceus cleanly partitions intertwined pointer flows, eliminating context explosion and improving both scalability and precision.
On 16 real-world Rust applications, Rceus outperforms state-of-the-art techniques - standard k-limiting, selective k-limiting for Java, and stack-filtered k-limiting for Rust - in both precision and efficiency. The evaluation includes Wasmtime, a WebAssembly runtime with 669K lines of code, where the benefits increase with program size. Rceus also composes with existing techniques, providing a practical and extensible foundation for scalable, precise Rust pointer analysis.
Cite as
Wenyao Chen, Wei Li, and Jingling Xue. Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.ECOOP.2026.1,
author = {Chen, Wenyao and Li, Wei and Xue, Jingling},
title = {{Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {1:1--1:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.1},
URN = {urn:nbn:de:0030-drops-260973},
doi = {10.4230/LIPIcs.ECOOP.2026.1},
annote = {Keywords: Pointer Analysis, Context Sensitivity, Rust}
}
Document
Automatic Layout of Railroad Diagrams
Abstract
Railroad diagrams (also called "syntax diagrams") are a common, intuitive visualization of grammars, but limited tooling and a lack of formal attention to their layout mostly confines them to hand-drawn documentation. We present the first formal treatment of railroad diagram layout along with a principled, practical implementation. We characterize the problem as compiling a diagram language (specifying conceptual components and how they connect and compose) to a layout language (specifying basic graphical shapes and their sizes and positions). We then implement a compiler that performs line wrapping to meet a target width, as well as vertical alignment and horizontal justification per user-specified policies. We frame line wrapping as optimization, where we describe principled dimensions of optimality and implement corresponding heuristics. For front-end evaluation, we show that our diagram language is well-suited for common applications by describing how regular expressions and Backus-Naur form can be compiled to it. For back-end evaluation, we argue that our compiler is practical by comparing its output to diagrams laid out by hand and by other tools.
Cite as
Shardul Chiplunkar and Clément Pit-Claudel. Automatic Layout of Railroad Diagrams. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 2:1-2:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chiplunkar_et_al:LIPIcs.ECOOP.2026.2,
author = {Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
title = {{Automatic Layout of Railroad Diagrams}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {2:1--2:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.2},
URN = {urn:nbn:de:0030-drops-260982},
doi = {10.4230/LIPIcs.ECOOP.2026.2},
annote = {Keywords: syntax diagram, graph layout, line wrapping, pretty-printing}
}
Document
Faster Verified Explanations for Neural Networks
Abstract
Verified explanations are a principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with an exponential worst-case complexity. We present FaVeX, a novel algorithm to compute verified explanations. FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. Furthermore, we present a novel and hierarchical definition of verified explanations, termed verifier-optimal robust explanations, that explicitly factors the incompleteness of network verifiers within the explanation. Our comprehensive experimental evaluation demonstrates the superior scalability of both FaVeX, and of verifier-optimal robust explanations, which together can produce meaningful formal explanation on networks with hundreds of thousands of non-linear activations.
Cite as
Alessandro De Palma, Greta Dolcetti, and Caterina Urban. Faster Verified Explanations for Neural Networks. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 3:1-3:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{depalma_et_al:LIPIcs.ECOOP.2026.3,
author = {De Palma, Alessandro and Dolcetti, Greta and Urban, Caterina},
title = {{Faster Verified Explanations for Neural Networks}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {3:1--3:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.3},
URN = {urn:nbn:de:0030-drops-260999},
doi = {10.4230/LIPIcs.ECOOP.2026.3},
annote = {Keywords: Verified Explanations, eXplainable Artificial Intelligence (XAI), Local Robustness, Neural Network Verification, Static Analysis}
}
Document
Efficient Symbolic Execution of Software Under Fault Attacks
Abstract
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing methods for analyzing the impact of maliciously injected hardware faults on the embedded software, they suffer from inaccurate fault modeling and inefficient fault analysis. To overcome these limitations, we propose two novel techniques. First, we propose a new fault modeling technique that leverages automated program transformation to add symbolic variables to the original program, to accurately model the new program behavior induced by the injected faults. This new fault modeling approach has two advantages over existing techniques: (a) the fault-induced program behavior is closely related to what attackers exploit in practice and (b) the automatically transformed program may be analyzed by any downstream fault analysis algorithm. Second, we propose an efficient symbolic execution algorithm that is designed specifically for conducting fault analysis on the transformed program. It leverages two pruning techniques to mitigate path explosion, which is the main performance bottleneck of symbolic execution in general and, in this particular application, is exacerbated by the additional fault-induced program behavior. We have implemented the proposed method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art techniques. Specifically, our method not only drastically reduces the overall running time of symbolic execution but also retains its error detection capabilities. Compared to the current state-of-the-art, it is able to detect previously-missed safety violations and at the same time avoid bogus violations. Furthermore, compared to the baseline algorithm, our optimized symbolic execution algorithm can be orders-of-magnitude faster.
Cite as
Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang. Efficient Symbolic Execution of Software Under Fault Attacks. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 4:1-4:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fang_et_al:LIPIcs.ECOOP.2026.4,
author = {Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
title = {{Efficient Symbolic Execution of Software Under Fault Attacks}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {4:1--4:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.4},
URN = {urn:nbn:de:0030-drops-261009},
doi = {10.4230/LIPIcs.ECOOP.2026.4},
annote = {Keywords: Symbolic Execution, Safety Verification, Fault Attack, Embedded Software}
}
Document
A Stable Lossless Syntax Tree for Real-Time Collaborative Programming
Abstract
Real-time collaborative programming tools synchronize source code as text, propagating keystrokes or text patches to other collaborators. This propagation of unstructured text often leads to syntactically invalid states, because edits take place by character position rather than by syntactic entity. Consequently, our key idea is to propagate syntactically valid changes only.
This paper contributes a structure-aware synchronization substrate based on two complementary representations and a propagation algorithm: (i) A Lossless Syntax Tree stores source code in structured form while preserving program trivia, like whitespace and comments. This is necessary because collaborators must be able to reconstruct byte-identical source text from propagated (structural) changes; (ii) A Stable Syntax Tree extends this representation with persistent node identifiers to enable robust structural diffing between successive versions; (iii) Our propagation algorithm derives deterministic structural edit scripts for the following operations: insert, delete, move, and update. The algorithm can be used across grammars, because a lightweight per-language specification guides the stable reuse of node identifiers.
The biggest achievement of our approach is to take unstructured text changes and extract structural edit operations that provide syntactically correct source code changes. We formalize our proposed representations, show how diffing extracts structural edits, and how these edit scripts are applied at the collaborator. Particularly complex is the resulting move of subtrees. Our approach minimizes within-parent move noise using a per-parent Longest Increasing Subsequence.
We evaluate our approach using two languages (Java and JavaScript), three file sizes (small/medium/large), and five edit scenarios. Across all scenarios we observe byte-identical collaboration, node identity stability, and deterministic edit scripts. We demonstrate that applying Longest Increasing Subsequence is necessary for canonical minimality under sibling moves. We furthermore demonstrate that tree diffing cost is structure-sensitive: per-node cost increases with sibling fanout rather than depth. 95th percentile (p95) of end-to-end latencies meet the ≤ 1 second delay budget for small and medium files in both languages. Large Java is near 1 second (p95 ≈ 1.22 seconds) while JavaScript exceeds the 2 seconds hard-cap (p95 ≈ 2.86 seconds). Overall, our approach provides a deterministic, language-portable substrate for structure-aware real-time collaborative programming that separates structural propagation from unstructured keystrokes to preserve code correctness and developer intent.
Cite as
Leon Freudenthaler and Karl Michael Göschka. A Stable Lossless Syntax Tree for Real-Time Collaborative Programming. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 5:1-5:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{freudenthaler_et_al:LIPIcs.ECOOP.2026.5,
author = {Freudenthaler, Leon and G\"{o}schka, Karl Michael},
title = {{A Stable Lossless Syntax Tree for Real-Time Collaborative Programming}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {5:1--5:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.5},
URN = {urn:nbn:de:0030-drops-261017},
doi = {10.4230/LIPIcs.ECOOP.2026.5},
annote = {Keywords: real-time collaborative programming, tree-based operations, structure-aware propagation, synchronous collaboration systems}
}
Document
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
Abstract
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT - a type system combining fractional ownership and refinement types for imperative program verification - with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.’s type system to support nested arrays by generalizing the notion of ownership to be able to refer to the indices of the outer arrays and prove the soundness of the extended type system. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.
Cite as
Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 6:1-6:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fujiwara_et_al:LIPIcs.ECOOP.2026.6,
author = {Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
title = {{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {6:1--6:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.6},
URN = {urn:nbn:de:0030-drops-261029},
doi = {10.4230/LIPIcs.ECOOP.2026.6},
annote = {Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}
Document
Compositional Design, Implementation, and Verification of Swarms
Abstract
Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.
Cite as
Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional Design, Implementation, and Verification of Swarms. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 7:1-7:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{furbach_et_al:LIPIcs.ECOOP.2026.7,
author = {Furbach, Florian and Clorius, Lucas and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
title = {{Compositional Design, Implementation, and Verification of Swarms}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {7:1--7:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.7},
URN = {urn:nbn:de:0030-drops-261036},
doi = {10.4230/LIPIcs.ECOOP.2026.7},
annote = {Keywords: Swarms, Swarm Protocols, Concurrency, Distributed Coordination, Local-first Software, Behavioural Types, Publish-Subscribe, Asynchronous Communication}
}
Document
Comparing Transparent Static Analyzers with Open Verification Dashboard
Abstract
Given an input program, sound static analyzers compute a list of potential runtime errors in it. However, measuring their precision and comparing their results remains challenging. In this work, we formalize a notion of transparent static analyzers that report the proof obligations they check, including both verified and unverified obligations. This transparent output enables a semantics-directed, fine-grained comparison and the combination of static analyzers. We introduce the Open Verification Dashboard (OVD), which provides a unified interface to aggregate the results of multiple static analyzers. By juxtaposing verified properties and outstanding warnings, OVD highlights coverage gaps, variabilities and inconsistencies across tools. We experimentally evaluate the benefits of OVD on benchmarks from the Competition on Software Verification (SV-COMP). This work paves the way for a static analysis standard for C runtime error reporting.
Cite as
Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 8:1-8:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{goalard_et_al:LIPIcs.ECOOP.2026.8,
author = {Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
title = {{Comparing Transparent Static Analyzers with Open Verification Dashboard}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {8:1--8:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.8},
URN = {urn:nbn:de:0030-drops-261049},
doi = {10.4230/LIPIcs.ECOOP.2026.8},
annote = {Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Document
Vardalith: Hybrid Detection of Persistent Memory Concurrency Bugs
Abstract
Persistent Memory offers byte-addressable persistence but exposes developers to new concurrency bugs - persistency-induced races - where a thread might read unpersisted data, potentially leading to inconsistencies after crashes. Existing tools face important practical limitations: they either require exhaustive exploration of thread interleavings, depend on application-specific semantics or specialized testing drivers, or report many interleavings that do not correspond to real persistency-induced races. This paper introduces a hybrid approach for detecting persistency-induced races that overcomes these limitations. Our method operates without application-specific knowledge and does not require observing the exact racy interleaving during testing. Instead, by precisely extending the detection window around persistent memory accesses, we can infer the existence of racy interleavings whenever conflicting executions are observed. Our evaluation across multiple applications found 26 bugs (7 new) demonstrating that our approach provides a principled and practical foundation for detecting persistency-induced races.
Cite as
João Gonçalves, José Fragoso Santos, Rodrigo Rodrigues, and Miguel Matos. Vardalith: Hybrid Detection of Persistent Memory Concurrency Bugs. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 9:1-9:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{goncalves_et_al:LIPIcs.ECOOP.2026.9,
author = {Gon\c{c}alves, Jo\~{a}o and Fragoso Santos, Jos\'{e} and Rodrigues, Rodrigo and Matos, Miguel},
title = {{Vardalith: Hybrid Detection of Persistent Memory Concurrency Bugs}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {9:1--9:34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.9},
URN = {urn:nbn:de:0030-drops-261052},
doi = {10.4230/LIPIcs.ECOOP.2026.9},
annote = {Keywords: persistent memory, concurrency, crash consistency}
}
Document
Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability
Abstract
IFDS taint analysis is inherently context- and flow-sensitive, allowing precise encoding of field sensitivity in access-path generation. However, preserving this level of precision in practice is difficult, leading to over-tainting - marking more data facts as tainted than necessary. The root cause is the undecidability of solving two context-free language reachability (CFL-reachability) problems along the same dataflow path, which forces k-limiting as an over-approximation of field sensitivity. Consequently, spurious access paths are introduced, increasing analysis time, memory usage, and false positives, especially in large-scale applications.
To address this challenge, we present TnFix, a CFL-reachability-based technique for mitigating over-tainting in IFDS taint analysis. The key insight is that the field sequence of any candidate tainted access path can be checked by a deterministic finite automaton (DFA) that accepts feasible sequences of field accesses. TnFix builds these DFAs by first solving a lightweight field-sensitive CFL-reachability problem to construct a Field Points-to Graph (FPG) that integrates data flows from taint sources and library summaries, and then converting the FPG into per-object DFAs. During taint analysis, TnFix queries these DFAs to prune access paths whose field sequences are rejected, eliminating the spurious paths introduced by k-limiting and improving precision without sacrificing scalability.
In a comparative evaluation against FlowDroid on a set of 36 widely used Android apps for taint analysis, TnFix successfully analyzes 7 apps that FlowDroid cannot complete within a three-hour time budget. For the remaining 29 apps, it improves analysis speed by an average of 2.5× and reduces false positives by an average of 12.2%. TnFix thus establishes the first CFL-based optimization framework for reducing over-tainting in IFDS taint analysis, delivering substantial gains in both efficiency and precision for practical use.
Cite as
Yujiang Gui, Yonggang Tao, and Jingling Xue. Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gui_et_al:LIPIcs.ECOOP.2026.10,
author = {Gui, Yujiang and Tao, Yonggang and Xue, Jingling},
title = {{Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {10:1--10:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.10},
URN = {urn:nbn:de:0030-drops-261068},
doi = {10.4230/LIPIcs.ECOOP.2026.10},
annote = {Keywords: Taint Analysis, CFL-Reachability, Access Path, Field Sensitivity, Pointer Analysis}
}
Document
A Complete Program Logic for Compositional Linearizability
Abstract
We present Linearizability Hoare Logic (LHL), the first mechanized, sound, and complete program logic for atomic, set, and interval linearizability. We achieve this by showing soundness and completeness of LHL w.r.t. a more general criterion, compositional linearizability, which subsumes all three criteria. We showcase the expressivity of LHL by verifying an exchanger with a set linearizable specification, the elimination-backoff stack built above the exchanger, a lock with an atomic linearized specification, and a write-snapshot object with an interval linearizable specification.
Together with LHL we formalize a modular verification framework for concurrent components based on the theory of compositional linearizability. This allows us to specify components at a high level of abstraction and granularity, and then assemble them into large systems that are correct by construction. As a showcase, we verify the elimination-backoff stack modularly by verifying each of its sub-components against their linearized specifications and then linking them together.
Cite as
Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. A Complete Program Logic for Compositional Linearizability. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hatti_et_al:LIPIcs.ECOOP.2026.11,
author = {Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
title = {{A Complete Program Logic for Compositional Linearizability}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {11:1--11:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.11},
URN = {urn:nbn:de:0030-drops-261075},
doi = {10.4230/LIPIcs.ECOOP.2026.11},
annote = {Keywords: Program Logic, Rely-Guarantee, Linearizability, Compositional Verification, Concurrency}
}
Document
Language-Integrated Recursive Queries
Abstract
Performance-critical applications, including large-scale program analyses, graph analyses, and distributed system analyses, rely on fixed-point computations. The introduction of recursion using the WITH RECURSIVE keyword in SQL:1999 extended the ability of relational database systems to handle fixed-point computations, unlocking significant performance advantages by allowing computation to move closer to the data. Yet, with recursion, SQL becomes a Turing-complete programming language with new correctness and safety risks.
Full SQL lacks a fixed semantics, as the SQL specification is written in natural language with ambiguities that database vendors resolve in divergent ways. As a result, reasoning about the correctness of recursive SQL programs must rely on isolated, composable properties of queries rather than wrestling a unified formal model out of a language with notoriously inconsistent implementations across systems. To address these challenges, we propose a calculus, λ_RQL, that derives properties from embedded recursive queries using the host-language type system and, depending on the database backend, rejects queries that may lead to the three classes of recursive query errors: runtime database exceptions, incorrect results, and nontermination. Queries that respect all properties are guaranteed to find the minimal fixed point in a finite number of steps. We introduce TyQL, a practical implementation in Scala for safe, recursive language-integrated query. TyQL uses modern type system features of Scala 3, namely Named-Tuples and type-level pattern matching, to ensure query portability and safety. TyQL shows no performance penalty compared to SQL queries expressed as embedded strings while enabling a three-order-of-magnitude speedup over non-recursive SQL.
Cite as
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky. Language-Integrated Recursive Queries. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 12:1-12:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{herlihy_et_al:LIPIcs.ECOOP.2026.12,
author = {Herlihy, Anna and Shaikhha, Amir and Ailamaki, Anastasia and Odersky, Martin},
title = {{Language-Integrated Recursive Queries}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {12:1--12:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.12},
URN = {urn:nbn:de:0030-drops-261086},
doi = {10.4230/LIPIcs.ECOOP.2026.12},
annote = {Keywords: Language-integrated query, embedded DSL, SQL, Scala, fixpoint, Datalog}
}
Document
Automated Inline-Test Generation without Relying on Method-Level Unit Tests
Abstract
Inline tests validate individual program statements and expressions, and they detect many seeded faults (i.e., mutants) that unit tests miss in these target statements. ExLi is the only automated inline-test generation technique today; it carves inline tests from method-level unit tests that are written for methods that enclose target statements. Thus, ExLi cannot work for target statements that method-level unit tests do not cover. Also, the quality of ExLi-generated inline tests depends on the quality of method-level unit tests. We propose Smack to generate inline tests without relying on method-level unit tests. Smack is inspired by how inline tests are run: each is extracted with the target statement and run independently. Smack exploits this independence. Smack first extracts each target statement into a new method. Next, Smack applies a unit-test generator to the extracted method, which tends to have simpler control flow than the target statement’s enclosing method and carves inline tests from them. Finally, Smack transplants the resulting inline tests to be right after the target statement in the original enclosing method. We evaluate Smack on the same 957 target statements in 31 open-source projects that ExLi was evaluated on. Smack generates inline tests for 277 of 312 (88.8%) statements that ExLi cannot handle. These inline tests kill 96.7% of 1,815 mutants in these 312 target statements. Therefore, Smack improves on ExLi by extending the reach and fault-detection ability of inline-test generation. Smack also generates inline tests for 609 of 645 (94.4%) target statements that ExLi can handle. Smack-generated inline tests kill 83.1% of 2,844 mutants in these 645 target statements. 147 of these killed mutants survive ExLi-generated inline tests. So, Smack is also complementary to ExLi on target statements that ExLi can handle.
Cite as
Pengyue Jiang, Yu Liu, Anna Guo, Milos Gligoric, and Owolabi Legunsen. Automated Inline-Test Generation without Relying on Method-Level Unit Tests. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 13:1-13:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jiang_et_al:LIPIcs.ECOOP.2026.13,
author = {Jiang, Pengyue and Liu, Yu and Guo, Anna and Gligoric, Milos and Legunsen, Owolabi},
title = {{Automated Inline-Test Generation without Relying on Method-Level Unit Tests}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {13:1--13:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.13},
URN = {urn:nbn:de:0030-drops-261090},
doi = {10.4230/LIPIcs.ECOOP.2026.13},
annote = {Keywords: Software testing, inline tests, automated test generation}
}
Document
The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State
Abstract
Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by isolated components. This works well as long as components do not share or expose their internal state: Any state update that is locally sound is also globally sound. However, some abstract domains require shared state, most prominently relational abstract domains, which use symbolic expressions such as 2x + 5 to represent abstract values. As the relational component performs a strong update of x, the abstract value 2x + 5 can change non-monotonically, which breaks soundness. We propose a novel solution to this problem: A virtual recency abstractions that decouples the relational component, supports strong updates, and allows recursion. We prove that the virtual recency abstraction restores soundness: Any shared state wrapped in our virtual recency abstraction may be locally updated non-monotonically, while global soundness persists. We applied our approach to develop the first relational WebAssembly analysis, reusing many components from an existing inter-procedural abstract interpreter. Furthermore, we evaluate the recall, precision, and scalibility of this analysis to demonstrate the practicality of the virtual recency abstraction.
Cite as
Sven Keidel, Raphaël Monat, and Sebastian Erdweg. The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{keidel_et_al:LIPIcs.ECOOP.2026.14,
author = {Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
title = {{The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {14:1--14:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.14},
URN = {urn:nbn:de:0030-drops-261103},
doi = {10.4230/LIPIcs.ECOOP.2026.14},
annote = {Keywords: Relational Numerical Analysis, Recency Abstraction}
}
Document
Automatic Code and Test Generation of Smart Contracts from Coordination Models
Abstract
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.
Cite as
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 15:1-15:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{konjohselabi_et_al:LIPIcs.ECOOP.2026.15,
author = {Konjoh Selabi, Elvis and Murgia, Maurizio and Ravara, Ant\'{o}nio and Tuosto, Emilio},
title = {{Automatic Code and Test Generation of Smart Contracts from Coordination Models}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {15:1--15:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.15},
URN = {urn:nbn:de:0030-drops-261119},
doi = {10.4230/LIPIcs.ECOOP.2026.15},
annote = {Keywords: Smart Contracts, Coordination Models, Formal Semantics, Role-Based Access, Decentralised Systems, Code Generation, Solidity, Verification}
}
Document
Characterizing Type Feedback in Just-In-Time Compilation
Abstract
Just-in-time (JIT) compilers leverage type feedback to optimize dynamic languages by recording runtime observations during interpretation and using them to generate specialized code. However, this recording process introduces significant execution time overhead to program warmup. This paper presents a characterization study of how feedback information is utilized by JIT compilers, providing motivation for future work on reducing recording overhead. We instrument the Ř compiler for the R language to track feedback slot usage throughout compilation, analyzing well-known benchmarks and real-world programs. Our measurements reveal that recording adds overhead to the interpreter up to 1.6× (mean 1.2×), yet at least 59% of non-empty slots are not used by the compiler. A large fraction of these unused slots can be attributed to dead code that the compiler eliminated. Most of the remaining slots are type-stable - meaning the inferred type matches the observed type - making speculation futile. To quantify the potential for improvement, we evaluate two oracle-based configurations that establish upper bounds on achievable reduction: a conservative set approach that preserves optimization quality while improving warmup, and an optimistic set approach that sacrifices some compiled code performance for faster interpretation.
Cite as
Sebastián Krynski, Filip Říha, Filip Křikava, and Jan Vitek. Characterizing Type Feedback in Just-In-Time Compilation. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{krynski_et_al:LIPIcs.ECOOP.2026.16,
author = {Krynski, Sebasti\'{a}n and \v{R}{\'\i}ha, Filip and K\v{r}ikava, Filip and Vitek, Jan},
title = {{Characterizing Type Feedback in Just-In-Time Compilation}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {16:1--16:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.16},
URN = {urn:nbn:de:0030-drops-261124},
doi = {10.4230/LIPIcs.ECOOP.2026.16},
annote = {Keywords: Feedback vector, JIT compilation, type speculation, deoptimization}
}
Document
NEST: Network Enforced Session Types
Abstract
This paper introduces NEST (Network Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior work that instruments or wraps application code, we synthesise packet-level monitors that enforce protocols directly in the data plane. We develop algorithms to generate network-level monitors from session types and extend them to handle packet loss and reordering. We implement NEST in P4 and evaluate it on applications including microservice and network-function models, showing that network-level monitors can enforce realistic non-trivial protocols.
Cite as
Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 17:1-17:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{larsen_et_al:LIPIcs.ECOOP.2026.17,
author = {Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
title = {{NEST: Network Enforced Session Types}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {17:1--17:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.17},
URN = {urn:nbn:de:0030-drops-261137},
doi = {10.4230/LIPIcs.ECOOP.2026.17},
annote = {Keywords: Session types, runtime verification, P4, programmable data planes}
}
Document
Eliminate Branches by Melding IR Instructions
Abstract
Branch mispredictions cause catastrophic performance penalties in modern processors, leading to performance loss. While hardware predictors and profile-guided techniques exist, data-dependent branches with irregular access patterns remain challenging. Traditional if-conversion eliminates branches via software predication but faces limitations on architectures like x86. It often fails on paths containing memory instructions or incurs excessive instruction overhead by fully speculating large branch bodies. This paper presents MERIT (MElding IR InsTructions), a compiler transformation that eliminates branches by aligning and melding similar operations from divergent paths at the IR instruction level. By observing that divergent paths often perform structurally similar operations with different operands, MERIT adapts sequence alignment to discover merging opportunities and employs safe operand-level guarding to ensure semantic correctness without hardware predication. Implemented as an LLVM pass and evaluated on 102 programs from four benchmark suites, MERIT achieves a 1.52× geometric mean speedup on 24 branch-heavy microbenchmarks (peak 32× on toUpper) and reduces branch mispredictions by 48.9% on average. On more realistic workloads - SPECrate 2017 (16 benchmarks), SQLite TPC-H (22 queries), and CPython pyperformance (40 benchmarks) - MERIT with profile-guided function selection achieves a positive geomean (∼1.01×) across all three suites, demonstrating consistent improvement without regressions.
Cite as
Yuze Li, Srinivasan Ramachandra Sharma, Charitha Saumya, Ali R. Butt, and Kirshanthan Sundararajah. Eliminate Branches by Melding IR Instructions. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 18:1-18:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{li_et_al:LIPIcs.ECOOP.2026.18,
author = {Li, Yuze and Sharma, Srinivasan Ramachandra and Saumya, Charitha and Butt, Ali R. and Sundararajah, Kirshanthan},
title = {{Eliminate Branches by Melding IR Instructions}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {18:1--18:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.18},
URN = {urn:nbn:de:0030-drops-261148},
doi = {10.4230/LIPIcs.ECOOP.2026.18},
annote = {Keywords: Control-flow Transformation, Branch Elimination}
}
Document
Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Abstract
This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided "proof certificate" of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack.
Cite as
Stian Lybech, Daniele Gorla, and Luca Aceto. Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 19:1-19:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lybech_et_al:LIPIcs.ECOOP.2026.19,
author = {Lybech, Stian and Gorla, Daniele and Aceto, Luca},
title = {{Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {19:1--19:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.19},
URN = {urn:nbn:de:0030-drops-261159},
doi = {10.4230/LIPIcs.ECOOP.2026.19},
annote = {Keywords: semantic typing, smart contracts, information flow control, non-interference}
}
Document
Verifying Wait-Freedom for Concurrent Higher-Order Programs
Abstract
Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order languages, verifying it for higher-order programming languages with general references remains an open challenge. In such languages, operations may be used by arbitrary, unverified higher-order clients, making it unclear how to even define wait-freedom formally in terms of programs' semantics, let alone prove it.
In this paper, we present the first framework for verifying wait-freedom of concurrent programs written in a higher-order language with general references. Our approach is based on the Lawyer concurrent separation logic which has been recently introduced for termination verification. We identify a specification pattern in the Lawyer logic that captures wait-freedom. To establish this connection formally, we prove a novel adequacy theorem for Lawyer which states that programs which are proven correct in the Lawyer logic against a specification in the aforementioned specification pattern are wait-free. Proving wait-freedom requires to show that all calls made to operations by any arbitrary client terminate. Thus, as a part of proving the adequacy theorem above, we need to prove that the behavior of the client of the data structure is safe in the sense that it does not break the internal invariants of the data structure, e.g., by directly manipulating the data structure’s internal state. To this end, we develop a logical relations model that establishes safety for all clients once and for all.
We demonstrate the effectiveness of our approach by proving wait-freedom for several representative examples, including a higher-order list map function, and a memory-efficient single-producer, single-consumer queue. For the latter, wait-freedom is conditional in that, as the name suggests, there can be at most one enqueuer thread and one dequeuer thread. To capture this formally, we introduce the notion of restricted wait-freedom as a variant of wait-freedom that restricts the number of concurrent threads, and show how our approach can support reasoning about restricted wait-freedom. All our results have been mechanized on top of the Rocq Prover and using the Iris separation logic framework that Lawyer is also based on.
Cite as
Egor Namakonov, Lars Birkedal, and Amin Timany. Verifying Wait-Freedom for Concurrent Higher-Order Programs. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 20:1-20:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{namakonov_et_al:LIPIcs.ECOOP.2026.20,
author = {Namakonov, Egor and Birkedal, Lars and Timany, Amin},
title = {{Verifying Wait-Freedom for Concurrent Higher-Order Programs}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {20:1--20:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.20},
URN = {urn:nbn:de:0030-drops-261164},
doi = {10.4230/LIPIcs.ECOOP.2026.20},
annote = {Keywords: separation logic, higher-order logic, concurrency, formal verification}
}
Document
Foundational and Compositional Verification of Layered Concurrent Objects
Abstract
Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However, vanilla verified layers come with global states which severely limit their extensibility. This problem may be solved by dividing a layer into objects with encapsulated local states. Although the idea has been successfully realized in the sequential setting, it remains unclear if it also works in a concurrent setting where function calls across layers are no longer atomic steps and foundational proofs are needed.
We propose an approach to foundational and compositional verification of concurrent objects organized into multiple layers. The central idea is to represent concurrent objects as open labeled transition systems with encapsulated threads and to adopt trace refinements as a uniform notion of functional correctness which supports both vertical composition (layered refinement) and horizontal composition (extension of layer interfaces). Due to the operational nature of transition systems, it is straightforward to adopt traditional simulation techniques to produce foundational proof certificates. We implement this framework in the Rocq theorem prover and demonstrate its capability in foundational and compositional verification by verifying non-trivial lock-free concurrent data structures.
Cite as
Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ni_et_al:LIPIcs.ECOOP.2026.21,
author = {Ni, Yicheng and Wang, Yuting},
title = {{Foundational and Compositional Verification of Layered Concurrent Objects}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {21:1--21:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.21},
URN = {urn:nbn:de:0030-drops-261171},
doi = {10.4230/LIPIcs.ECOOP.2026.21},
annote = {Keywords: Concurrency, Compositional Verification}
}
Document
Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages
Abstract
Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their specification, they may not fully understand the language of the output, there may be systematic misconceptions suffered by the user and perhaps even embedded in the language model, and so on.
Responsible use of GenAI requires humans in the loop. To be effective, the human interaction must be both meaningful and moderate. We accomplish this as follows. First, we generate multiple candidate expressions instead of one. We then use formal language containment properties to generate distinguishing concrete scenarios that illustrate the differences between the candidates. We then have users rate these concrete scenarios. This process converges in a few steps, while also giving the user insight into any lack of clarity on their part.
We have built a tool, pick, that implements this iterative process. We apply it to three formal languages with the necessary properties: regexes, linear temporal logic, and access-control policies. We show through experiments that pick is a significant improvement over showing users the candidate expressions, and also helps catch situations where no output is a match.
Cite as
Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 22:1-22:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{prasad_et_al:LIPIcs.ECOOP.2026.22,
author = {Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
title = {{Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {22:1--22:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.22},
URN = {urn:nbn:de:0030-drops-261181},
doi = {10.4230/LIPIcs.ECOOP.2026.22},
annote = {Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}
Document
Scaling Bottom-Up IFDS Taint Analysis with Optimized Data-Flow Encoding
Abstract
Static taint analysis is an important technique for bug-finding and vulnerability detection on source-code. One commonly used technique to solve inter-procedural taint analysis problems is the well-studied Interprocedural Finite Distributive Subsets (IFDS) algorithm. However, when performing a whole-program analysis, IFDS-based taint analyses have trouble scaling to large target programs, mainly due to its huge memory consumption. A common technique to solve this issue is to modularize the analysis by visiting the call graph bottom-up, performing local sub-analyses in isolation. Still, bottom-up formulations of IFDS are rare due to their own scalability issues caused by over-approximating the analysis state at the beginning of a procedure. In this work we study how one can improve scalability for bottom-up taint analysis of C and C++ programs on millions of lines of code. We present MonoIFDS, a variant of the IFDS algorithm that combines IFDS-style procedure summaries with bottom-up inter-procedural propagation. It uses a modified encoding of the data-flow state and propagation to improve the efficiency of handling large analysis states, and to enable optimizations, such as optimizing the iteration order, that were not beneficial on IFDS analyses before. In our evaluation we show, how MonoIFDS performs compared to SparseIFDS when analyzing real-world C and C++ programs. Achieving a speedup of 6.17 on average with only consuming 51% of the memory compared to SparseIFDS, MonoIFDS drastically outperforms the state-of-the-art SparseIFDS and enables developers to target the analysis of large programs on consumer hardware.
Cite as
Fabian Schiebel and Eric Bodden. Scaling Bottom-Up IFDS Taint Analysis with Optimized Data-Flow Encoding. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{schiebel_et_al:LIPIcs.ECOOP.2026.23,
author = {Schiebel, Fabian and Bodden, Eric},
title = {{Scaling Bottom-Up IFDS Taint Analysis with Optimized Data-Flow Encoding}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {23:1--23:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.23},
URN = {urn:nbn:de:0030-drops-261194},
doi = {10.4230/LIPIcs.ECOOP.2026.23},
annote = {Keywords: Static analysis, IFDS, C/C++}
}
Document
Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution
Abstract
Record/Replay (RR) allows developers to record an execution and then replay it exactly as it was recorded. RR enables deterministic replay of non-deterministic behaviors in a different environment than the one used for the recording, which can capture complex bugs in production and find the root cause during development. Unfortunately, support for RR still introduces a non-negligible amount of performance overhead, which limits its applicability. Two main sources of such overhead in state-of-the-art RR systems are: multi-threading, and I/O bound workloads. To ensure high-fidelity when replaying multi-threading execution, recordings either capture the total order of events, which the replayer then enforces, or capture a partial order that requires further processing before replay. Recording also effectively doubles the I/O performed as the recorder needs to perform the original I/O and then record it to a log. Such increased I/O severely limits the performance of I/O dominated workloads.
In this paper, we present two complimentary techniques to reduce the overhead of RR. First, we introduce Relaxed Total Order (RTO), an online-computable weakening of total order that preserves the cross-thread constraints needed for replay while avoiding unnecessary serialization. We design RTO to be compatible with Multi-Version eXecution (MVX), enabling online deterministic replay without pre-processing the recording log or heavyweight coordination. We formalize RTO’s strictness and correctness, showing that it is a novel point between partial- and total-order. Our prototype implementation on top of an existing state-of-the-art RR system reduces recording overhead from 21.0% to 15.3% and halves replay overhead from 67.5% to 31.7%.
Second, we combine RR with Multi-Version eXecution (MVX) to eliminate RR’s poor performance on I/O-bound workloads. Our hybrid design uses a follower variant to absorb the extra I/O needed for logging, and to backfill as much I/O as possible from the same underlying system, keeping the user-facing leader off the critical path. Our prototype reduces the overhead required to record I/O bound programs from 192.5% to just 25.5%, without penalizing other more common workloads. Together, RTO and hybrid MVX/RR substantially narrow the gap between today’s RR systems and practical, low-overhead, always-on deployment.
Cite as
David Schwartz and Luís Pina. Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 24:1-24:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{schwartz_et_al:LIPIcs.ECOOP.2026.24,
author = {Schwartz, David and Pina, Lu{\'\i}s},
title = {{Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {24:1--24:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.24},
URN = {urn:nbn:de:0030-drops-261207},
doi = {10.4230/LIPIcs.ECOOP.2026.24},
annote = {Keywords: Record Replay, Multi-version Execution, Java Virtual Machine}
}
Document
Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-Browser Cryptomining
Abstract
The decentralized and unregulated nature of cryptocurrencies, combined with their monetary value, has made them a vehicle for various illicit activities. One such activity is cryptojacking, an attack that uses stolen computing resources to mine cryptocurrencies without consent for profit. In-browser cryptojacking malware exploits high-performance web technologies such as WebAssembly to mine cryptocurrencies directly within the browser without file downloads. Although existing methods for cryptomining detection report high accuracy and low overhead, they are often susceptible to various forms of obfuscation, and due to the limited variety of cryptomining scripts in the wild, standard code obfuscation methods present a natural and appealing solution to avoid detection. To address these limitations, we propose using instruction-level data-flow graphs to detect cryptomining behavior. Data-flow graphs offer detailed structural insights into a program’s computations, making them suitable for characterizing proof-of-work algorithms, but they can be difficult to analyze due to their large size and susceptibility to noise and fragmentation under obfuscation. We present two techniques to simplify and compare data-flow graphs: (1) a graph simplification algorithm to reduce the computational burden of processing large and granular data-flow graphs while preserving local substructures; and (2) a subgraph similarity measure, the n-fragment inclusion score, based on fragment inclusion that is robust against noise and obfuscation. Using data-flow graphs as computation fingerprints, our detection framework PoT (Proof-of-Theft) was able to achieve high detection accuracy against standard obfuscations, outperforming existing detection methods.
Cite as
Tanapoom Sermchaiwong and Jiasi Shen. Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-Browser Cryptomining. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 25:1-25:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sermchaiwong_et_al:LIPIcs.ECOOP.2026.25,
author = {Sermchaiwong, Tanapoom and Shen, Jiasi},
title = {{Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-Browser Cryptomining}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {25:1--25:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.25},
URN = {urn:nbn:de:0030-drops-261211},
doi = {10.4230/LIPIcs.ECOOP.2026.25},
annote = {Keywords: software security, cryptocurrency, malware detection, dynamic analysis, data-flow graph}
}
Document
A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference
Abstract
In standard Java, wildcards behave like existential types: they must be opened before use in a method invocation, a process the compiler performs implicitly via capture conversion. We present Java-TX, a dialect of Java that sidesteps this existential encoding and treats wildcards as placeholders for unknown types, used directly without prior opening. This choice simplifies the type system and makes it compatible with an existing global type inference algorithm. The trade-off is that some method calls valid in standard Java become unavailable in Java-TX. In effect, we trade some of Java’s wildcard expressiveness for global type inference.
We explore the metatheory of Java-TX through Featherweight Java-TX (FJ-TX), a functional core calculus for Java-TX that extends Featherweight Generic Java with our wildcard interpretation. We prove type soundness for FJ-TX. Finally, we evaluate the practical impact of omitting capture conversion by conducting a study on open-source Java projects by calculating an underapproximation of how much existing Java code is compatible with the Java-TX type system.
Cite as
Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 26:1-26:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{stadelmeier_et_al:LIPIcs.ECOOP.2026.26,
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
title = {{A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {26:1--26:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.26},
URN = {urn:nbn:de:0030-drops-261229},
doi = {10.4230/LIPIcs.ECOOP.2026.26},
annote = {Keywords: type inference, Java, subtyping, wildcards, capture conversion}
}
Document
Remote Concolic Multiverse Debugging
Abstract
Debugging nondeterministic programs is inherently difficult, particularly in microcontroller environments where execution paths can diverge unpredictably due to external sensor inputs. Traditional debugging techniques often fail to capture or reproduce this nondeterministic behavior effectively. Multiverse debugging has emerged as a compelling technique to debug nondeterministic programs, allowing developers to systematically explore all possible execution paths. Unfortunately, current multiverse debuggers are snapshot-based and most operate over a model of the program, which limits their use for debugging resource-constrained microcontrollers. Additionally, current multiverse debuggers, even ones specifically designed for microcontrollers suffer from state explosion making the state space overwhelming during debugging.
To address these challenges, we introduce a trace-based multiverse debugger with a novel state-space reduction technique based on concolic execution. Our approach interleaves concolic analysis with live debugging to identify input values that define unique program paths. This hybrid technique efficiently prunes redundant paths from the state space while ensuring full code coverage. Unlike MIO, a recently published multiverse debugger for microcontrollers that focuses on IO consistency, our approach directly targets state explosion by leveraging concolic execution and uses a trace-based approach, significantly reducing the memory and communication overhead.
We implemented a prototype using the WARDuino WebAssembly virtual machine on an STM32 microcontroller, demonstrating the feasibility and efficiency of our approach in real-world scenarios. Our results highlight substantial reductions in the state space compared to traditional multiverse debugging. This makes multiverse debugging more accessible and efficient for developers working with complex, nondeterministic programs running on microcontrollers.
Cite as
Maarten Steevens, Tom Lauwaerts, and Christophe Scholliers. Remote Concolic Multiverse Debugging. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 27:1-27:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{steevens_et_al:LIPIcs.ECOOP.2026.27,
author = {Steevens, Maarten and Lauwaerts, Tom and Scholliers, Christophe},
title = {{Remote Concolic Multiverse Debugging}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {27:1--27:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.27},
URN = {urn:nbn:de:0030-drops-261238},
doi = {10.4230/LIPIcs.ECOOP.2026.27},
annote = {Keywords: Multiverse Debugging, Embedded devices, WebAssembly}
}
Document
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
Abstract
When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before actual computation. For this purpose, some languages provide dependent types such as Mat m n, and others offer refinement types to track predicates for shapes. Despite the theoretical maturity, however, such methods are often unhandy for continuous software development due to the requirement of proofs for judging type equality or subtyping; even automated proving is often unsuitable due to its unforeseeable time consumption. To remedy this, our study provides an alternative formalization by using staging. Based on the observation that conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases, we ensure such consistency by assertions evaluated as compile-time computations, not by proofs. Under this formalization, we can verify the consistency virtually statically in the sense that inconsistencies will be immediately detected as failures during compile-time computation. Our work achieves a mathematical guarantee that successfully generated code is always consistent with respect to tensor shapes. Furthermore, to vastly lessen the burden of adding shape- or stage-related descriptions, we (1) allow shape-related arguments to be implicit and infer them in a best-effort manner, and (2) offer a non-staged surface language that seemingly resembles ordinary dependently-typed languages and translate its programs into the staged core language. By a prototype implementation, we confirm that our language is expressive enough to verify a number of programs, including several examples offered by ocaml-torch.
Cite as
Takashi Suwa and Atsushi Igarashi. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 28:1-28:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{suwa_et_al:LIPIcs.ECOOP.2026.28,
author = {Suwa, Takashi and Igarashi, Atsushi},
title = {{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {28:1--28:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.28},
URN = {urn:nbn:de:0030-drops-261247},
doi = {10.4230/LIPIcs.ECOOP.2026.28},
annote = {Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}
Document
DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis
Abstract
Data containers, such as lists, arrays, trees, etc, raise challenges for program verification. In static analysis by abstract interpretation, one popular approach is summarization: multiple elements of a data structure are abstracted into a single one, favoring performance over precision. This technique is at the core of most container abstractions - from smashing to segmentation - of arrays, lists or algebraic data types.
However, summarization approaches are unable to express relations between containers, even when relational numerical abstract domains are used. Our work introduces DelExp, a new domain able to express relations between summarized variables. DelExp can state that the content of a data structure is included in the content of another data structure, up to a given transformation. DelExp is language-agnostic, modular in the abstraction chosen for any other types (integers, strings, functions, etc.), and can be seamlessly combined with existing container abstractions. We show how DelExp allows us to infer precise summaries for compositional analyses of container-manipulating functions in a pure functional language. We present extensions to DelExp supporting polymorphism and higher-order transformations.
Our implementation of DelExp within the MOPSA static analysis platform confirms that DelExp works out of the box with pre-existing container abstractions. Our evaluation targets both Python programs manipulating lists and relational summary generation for OCaml functions handling algebraic data types.
Cite as
Milla Valnet, Raphaël Monat, and Antoine Miné. DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 29:1-29:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{valnet_et_al:LIPIcs.ECOOP.2026.29,
author = {Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
title = {{DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {29:1--29:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.29},
URN = {urn:nbn:de:0030-drops-261257},
doi = {10.4230/LIPIcs.ECOOP.2026.29},
annote = {Keywords: Static Value Analysis, Abstract Interpretation, Functional Programming}
}
Document
Pearl/Brave New Idea
A Simple Recipe for Writing Decent Recursive Descent Parsers (Pearl/Brave New Idea)
Abstract
Parsing well-designed computer languages should not be a hard problem, be it for humans or for machines. This is not a new idea: in 1973, Vaughan R. Pratt argued against formalistic grammar specifications and in favor of a more intuitive and meaningful approach to designing and parsing syntax. In this Pearl, we take the reader on a journey through handwritten recursive descent parsing, revisiting Pratt’s original philosophy in a modern, statically-typed functional programming language. Contrary to many existing tutorials on the subject, we do not stop at simple expression languages: we also discuss how to tackle the full syntax of a simple programming language while avoiding the pitfalls of ad-hoc implementations. Indeed, a downside of recursive descent parsing is that the specification of what the parser accepts is written in code, which may contain subtle bugs and is not easily accessible to end users. We describe a simple recipe for architecting extensible recursive descent parsers that can automatically produce a readable representation of the syntax specification. We illustrate our approach by implementing a parser for a variant of Caml Light. Overall, this paper serves both as a pedagogical introduction to Pratt parsing in a modern programming language and as a practical guide to programmers who just want to implement, without unnecessary headaches, a computer language that is easy to parse and easy to read.
Cite as
Luyu Cheng and Lionel Parreaux. A Simple Recipe for Writing Decent Recursive Descent Parsers (Pearl/Brave New Idea). In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cheng_et_al:LIPIcs.ECOOP.2026.30,
author = {Cheng, Luyu and Parreaux, Lionel},
title = {{A Simple Recipe for Writing Decent Recursive Descent Parsers}},
booktitle = {40th European Conference on Object-Oriented Programming (ECOOP 2026)},
pages = {30:1--30:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-423-9},
ISSN = {1868-8969},
year = {2026},
volume = {372},
editor = {Krebbers, Robbert and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.30},
URN = {urn:nbn:de:0030-drops-261261},
doi = {10.4230/LIPIcs.ECOOP.2026.30},
annote = {Keywords: Parsing, Pratt Parsing, Operator Precedence, Recursive Descent}
}