45 Search Results for "Krebbers, Robbert"

Volume

LIPIcs, Volume 372

40th European Conference on Object-Oriented Programming (ECOOP 2026)

ECOOP 2026, Brussels, Belgium, June 29 to July 3, 2026

Editors: Robbert Krebbers and Alexandra Silva

Document
Complete Volume
DOI: 10.4230/LIPIcs.ECOOP.2026
LIPIcs, Volume 372, ECOOP 2026, Complete Volume

Authors: Robbert Krebbers and Alexandra Silva

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Robbert Krebbers and Alexandra Silva

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.1
Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis

Authors: Wenyao Chen, Wei Li, and Jingling Xue

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.2
Automatic Layout of Railroad Diagrams

Authors: Shardul Chiplunkar and Clément Pit-Claudel

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.3
Faster Verified Explanations for Neural Networks

Authors: Alessandro De Palma, Greta Dolcetti, and Caterina Urban

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.4
Efficient Symbolic Execution of Software Under Fault Attacks

Authors: Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.5
A Stable Lossless Syntax Tree for Real-Time Collaborative Programming

Authors: Leon Freudenthaler and Karl Michael Göschka

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.6
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Authors: Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.7
Compositional Design, Implementation, and Verification of Swarms

Authors: Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.8
Comparing Transparent Static Analyzers with Open Verification Dashboard

Authors: Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.9
Vardalith: Hybrid Detection of Persistent Memory Concurrency Bugs

Authors: João Gonçalves, José Fragoso Santos, Rodrigo Rodrigues, and Miguel Matos

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.10
Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability

Authors: Yujiang Gui, Yonggang Tao, and Jingling Xue

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.11
A Complete Program Logic for Compositional Linearizability

Authors: Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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
DOI: 10.4230/LIPIcs.ECOOP.2026.12
Language-Integrated Recursive Queries

Authors: Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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}
}
  • Refine by Type
  • 44 Document/PDF
  • 8 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 33 2026
  • 9 2025
  • 1 2024
  • 1 2023
  • 1 2022

  • Refine by Author
  • 5 Krebbers, Robbert
  • 3 Monat, Raphaël
  • 2 Igarashi, Atsushi
  • 2 Jacobs, Jules
  • 2 Scalas, Alceste
  • Show More...

  • Refine by Series/Journal
  • 43 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 6 Software and its engineering → Software testing and debugging
  • 6 Theory of computation → Program verification
  • 6 Theory of computation → Type theory
  • 5 Theory of computation → Program analysis
  • 4 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 3 Concurrency
  • 3 Iris
  • 3 Program Verification
  • 3 Separation Logic
  • 3 concurrency
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact