Issue
DARTS, Volume 12, Issue 1
Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)
-
Part of:
Volume:
DARTS, Volume 12 (ECRTS 2026)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2026-06-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{stievenart_et_al:DARTS.12.1.0,
author = {Sti\'{e}venart, Quentin and Zakowski, Yannick},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Sti\'{e}venart, Quentin and Zakowski, Yannick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.0},
URN = {urn:nbn:de:0030-drops-267333},
doi = {10.4230/DARTS.12.1.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
Eliminate Branches by Melding IR Instructions (Artifact)
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 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 Eliminate Branches by Melding IR Instructions (MERIT), 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 geometric mean speedup of 1.51× on 24 branch-heavy microbenchmarks (peak 32× on toUpper), reducing branch mispredictions by 48% on average. On realistic workloads - SPECrate 2017 (16 benchmarks), SQLite TPC-H (22 queries), and CPython pyperformance (40 benchmarks) - MERIT with profile-guided function selection achieves ∼1% geometric mean speedup across all three suites, demonstrating consistent improvement without regressions on diverse production workloads.
Cite as
Yuze Li, Srinivasan Ramachandra Sharma, Charitha Saumya, Ali R. Butt, and Kirshanthan Sundararajah. Eliminate Branches by Melding IR Instructions (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 1:1-1:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{li_et_al:DARTS.12.1.1,
author = {Li, Yuze and Sharma, Srinivasan Ramachandra and Saumya, Charitha and Butt, Ali R. and Sundararajah, Kirshanthan},
title = {{Eliminate Branches by Melding IR Instructions (Artifact)}},
pages = {1:1--1:9},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Li, Yuze and Sharma, Srinivasan Ramachandra and Saumya, Charitha and Butt, Ali R. and Sundararajah, Kirshanthan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.1},
URN = {urn:nbn:de:0030-drops-261381},
doi = {10.4230/DARTS.12.1.1},
annote = {Keywords: Branch elimination, Compiler transformation, LLVM-IR}
}
Document
Artifact
NEST: Network Enforced Session Types (Artifact)
Abstract
This artifact contains NEST: a tool for synthesizing network-level runtime monitors from application-level protocols specified as session types. More specifically, NEST takes as input one or more session types, and generates (1) a set of table entries to be uploaded on network switches that support the P4 standard, and (2) a Python API allowing applications to send/receive messages that carry the packet headers required for the network-level monitoring to work. This artifact also contains the code for reproducing the examples and measurements in the companion paper.
Cite as
Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{larsen_et_al:DARTS.12.1.2,
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 (Artifact)}},
pages = {2:1--2:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.2},
URN = {urn:nbn:de:0030-drops-261392},
doi = {10.4230/DARTS.12.1.2},
annote = {Keywords: Session types, runtime verification, P4, programmable data planes.}
}
Document
Artifact
The Virtual Recency Abstraction (Artifact)
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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{keidel_et_al:DARTS.12.1.3,
author = {Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
title = {{The Virtual Recency Abstraction (Artifact)}},
pages = {3:1--3:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.3},
URN = {urn:nbn:de:0030-drops-261405},
doi = {10.4230/DARTS.12.1.3},
annote = {Keywords: Relational Numerical Analysis, Recency Abstraction}
}
Document
Artifact
Characterizing Type Feedback in Just-in-Time Compilation (Artifact)
Abstract
This artifact provides the means to validate and reproduce the results of the associated paper "Characterizing Type Feedback in Just-in-Time Compilation". It enables to reproduce experimental claims made in the paper, including the claimed numbers and contained figures.
Cite as
Sebastián Krynski, Filip Říha, Filip Křikava, and Jan Vitek. Characterizing Type Feedback in Just-in-Time Compilation (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{krynski_et_al:DARTS.12.1.4,
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 (Artifact)}},
pages = {4:1--4:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Krynski, Sebasti\'{a}n and \v{R}{\'\i}ha, Filip and K\v{r}ikava, Filip and Vitek, Jan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.4},
URN = {urn:nbn:de:0030-drops-261415},
doi = {10.4230/DARTS.12.1.4},
annote = {Keywords: Feedback vector, JIT compilation, type speculation, deoptimization}
}
Document
Artifact
A Complete Program Logic for Compositional Linearizability (Artifact)
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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{hatti_et_al:DARTS.12.1.5,
author = {Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
title = {{A Complete Program Logic for Compositional Linearizability (Artifact)}},
pages = {5:1--5:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.5},
URN = {urn:nbn:de:0030-drops-261428},
doi = {10.4230/DARTS.12.1.5},
annote = {Keywords: Program Logic, Rely-Guarantee, Linearizability, Compositional Verification, Concurrency}
}
Document
Artifact
Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact)
Abstract
This artifact accompanies the eponymous article. It enables reproduction of the experimental claims made in the article that are covered by this description.
Cite as
Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{goalard_et_al:DARTS.12.1.6,
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 (Artifact)}},
pages = {6:1--6:15},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.6},
URN = {urn:nbn:de:0030-drops-261430},
doi = {10.4230/DARTS.12.1.6},
annote = {Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Document
Artifact
Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)
Abstract
This artifact accompanies the paper Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. It provides (1) the pick VS Code extension for regex synthesis with human-in-the-loop validation, and (2) anonymized user-study data and Docker images that reproduce the study interfaces and statistical analyses reported in the paper.
Cite as
Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 7:1-7:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{prasad_et_al:DARTS.12.1.7,
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 (Artifact)}},
pages = {7:1--7:9},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.7},
URN = {urn:nbn:de:0030-drops-261445},
doi = {10.4230/DARTS.12.1.7},
annote = {Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}
Document
Artifact
Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution (Artifact)
Abstract
Support for Record Replayer (RR) 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 address the former, 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. RTO is compatible with Multi-Version eXecution (MVX), enabling online deterministic replay without pre-processing the recording log or heavyweight coordination. To address the latter, 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 overhead needed for logging and I/O, keeping the user-facing leader off the critical path. The artifact contains the source code of our prototype, software used to evaluate the techniques' performance, and scripts to automate and summarize the results.
Cite as
David Schwartz and Luís Pina. Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{schwartz_et_al:DARTS.12.1.8,
author = {Schwartz, David and Pina, Lu{\'\i}s},
title = {{Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution (Artifact)}},
pages = {8:1--8:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Schwartz, David and Pina, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.8},
URN = {urn:nbn:de:0030-drops-261451},
doi = {10.4230/DARTS.12.1.8},
annote = {Keywords: Record Replay, Multi-Version eXecution, Relaxed Total Order, Concurrency, Hybrid MVX/RR}
}
Document
Artifact
Language-Integrated Recursive Queries (Artifact)
Abstract
This artifact accompanies the paper "Language-Integrated Recursive Queries," which introduces λ_RQL, a calculus that derives properties of embedded recursive queries from the host-language type system, and TyQL, its Scala 3 implementation. The artifact provides Docker image that runs the 16-query Recursive Query Benchmark (RQB) via JMH and produces CSV files containing the benchmark results.
Cite as
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky. Language-Integrated Recursive Queries (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 9:1-9:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{herlihy_et_al:DARTS.12.1.9,
author = {Herlihy, Anna and Shaikhha, Amir and Ailamaki, Anastasia and Odersky, Martin},
title = {{Language-Integrated Recursive Queries (Artifact)}},
pages = {9:1--9:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Herlihy, Anna and Shaikhha, Amir and Ailamaki, Anastasia and Odersky, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.9},
URN = {urn:nbn:de:0030-drops-261463},
doi = {10.4230/DARTS.12.1.9},
annote = {Keywords: Language-Integrated Query, Embedded DSL, SQL, Scala, Fixpoint, Datalog}
}
Document
Artifact
Efficient Symbolic Execution of Software under Fault Attacks (Artifact)
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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 10:1-10:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{fang_et_al:DARTS.12.1.10,
author = {Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
title = {{Efficient Symbolic Execution of Software under Fault Attacks (Artifact)}},
pages = {10:1--10:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.10},
URN = {urn:nbn:de:0030-drops-261477},
doi = {10.4230/DARTS.12.1.10},
annote = {Keywords: Symbolic Execution, Safety Verification, Fault Attack, Embedded Software}
}
Document
Artifact
Remote Concolic Multiverse Debugging (Artifact)
Abstract
This artifact accompanies our work "Remote Concolic Multiverse Debugging". In this work we present a novel multiverse debugger capable of effectively pruning redundant paths from the state space to reduce the effect of state explosion. This is accomplished by leveraging the power of concolic execution which is able to reduce the number of paths while ensuring full code coverage. Additionally, this work uses a trace-based approach which significantly reduces the overhead of multiverse debugging. This approach differs from previous works such as MIO, which uses a snapshot-based approach and focuses on IO consistency instead of the state explosion problem.
The artifact consists of three components which are bundled in the form of a VM image. This image consists of our prototype Remote Concolic Multiverse Debugger, an evaluation of our state-space reduction system and a performance comparison between trace and snapshot-based approaches.
Cite as
Maarten Steevens, Tom Lauwaerts, and Christophe Scholliers. Remote Concolic Multiverse Debugging (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 11:1-11:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{steevens_et_al:DARTS.12.1.11,
author = {Steevens, Maarten and Lauwaerts, Tom and Scholliers, Christophe},
title = {{Remote Concolic Multiverse Debugging (Artifact)}},
pages = {11:1--11:8},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Steevens, Maarten and Lauwaerts, Tom and Scholliers, Christophe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.11},
URN = {urn:nbn:de:0030-drops-261486},
doi = {10.4230/DARTS.12.1.11},
annote = {Keywords: Multiverse Debugging, Embedded devices, WebAssembly}
}
Document
Artifact
Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis (Artifact)
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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{chen_et_al:DARTS.12.1.12,
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 (Artifact)}},
pages = {12:1--12:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Chen, Wenyao and Li, Wei and Xue, Jingling},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.12},
URN = {urn:nbn:de:0030-drops-261496},
doi = {10.4230/DARTS.12.1.12},
annote = {Keywords: Pointer Analysis, Context Sensitivity, Rust}
}
Document
Artifact
Automatic Layout of Railroad Diagrams (Artifact)
Abstract
This artifact contains a Scala implementation of the algorithm described in the accompanying paper, and all resources and instructions necessary to verify the experimental claims made in the paper. The artifact is provided as a Docker image for reproducability. Separately, the latest state of development, which may have diverged from the claims supported by the artifact, can be found at https://github.com/epfl-systemf/librrd.
Cite as
Shardul Chiplunkar and Clément Pit-Claudel. Automatic Layout of Railroad Diagrams (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 13:1-13:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{chiplunkar_et_al:DARTS.12.1.13,
author = {Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
title = {{Automatic Layout of Railroad Diagrams (Artifact)}},
pages = {13:1--13:8},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Chiplunkar, Shardul and Pit-Claudel, Cl\'{e}ment},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.13},
URN = {urn:nbn:de:0030-drops-261509},
doi = {10.4230/DARTS.12.1.13},
annote = {Keywords: syntax diagram, graph layout, line wrapping, pretty-printing}
}
Document
Artifact
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)
Abstract
Based on the method proposed in the corresponding paper, we implemented a prototype type-checker (and a simple interpreter) for compile-time tensor shape checking. we ported a number of DNN-related example programs offered by ocaml-torch to our language and checked them by using the prototype implementation. The results indicated that our method can be considered effective enough to accommodate realistic tensor-handling programs.
Cite as
Takashi Suwa. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{suwa:DARTS.12.1.14,
author = {Suwa, Takashi},
title = {{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)}},
pages = {14:1--14:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Suwa, Takashi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.14},
URN = {urn:nbn:de:0030-drops-261517},
doi = {10.4230/DARTS.12.1.14},
annote = {Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}
Document
Artifact
DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact)
Abstract
This artifact accompanies the submission entitled "DelExp: a Relational Container Abstraction with Applications to Compositional Analysis. It enables to reproduce experimental claims made in the paper. The artifact requires a computer with Docker installed.
Cite as
Milla Valnet, Raphaël Monat, and Antoine Miné. DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 15:1-15:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{valnet_et_al:DARTS.12.1.15,
author = {Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
title = {{DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact)}},
pages = {15:1--15:7},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.15},
URN = {urn:nbn:de:0030-drops-261523},
doi = {10.4230/DARTS.12.1.15},
annote = {Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
Artifact
Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)
Abstract
This document provides artifact description for the ECOOP 2026 paper "Foundational and Compositional Verification of Layered Concurrent Objects".
Cite as
Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{ni_et_al:DARTS.12.1.16,
author = {Ni, Yicheng and Wang, Yuting},
title = {{Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)}},
pages = {16:1--16:11},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Ni, Yicheng and Wang, Yuting},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.16},
URN = {urn:nbn:de:0030-drops-261531},
doi = {10.4230/DARTS.12.1.16},
annote = {Keywords: Formal Verification, Concurrency, Formalization, Rocq}
}
Document
Artifact
A Simple Recipe for Writing Decent Recursive Descent Parsers (Artifact)
Abstract
This artifact consists of the MLscript implementation of the generalized Pratt parser introduced in the related article, together with a standalone browser demo written in MLscript. The demo parses full Caml Light programs, a lightweight precursor to OCaml, as well as examples with dynamically extended syntax, and displays syntax trees, tokens, parser traces, precedence information, syntax diagrams, and parser errors. For convenience, the package also includes the MLscript compiler project used to rebuild the parser and demo, and the tests that exercise the examples and generated web-demo artifacts.
Cite as
Luyu Cheng and Lionel Parreaux. A Simple Recipe for Writing Decent Recursive Descent Parsers (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 17:1-17:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{cheng_et_al:DARTS.12.1.17,
author = {Cheng, Luyu and Parreaux, Lionel},
title = {{A Simple Recipe for Writing Decent Recursive Descent Parsers (Artifact)}},
pages = {17:1--17:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Cheng, Luyu and Parreaux, Lionel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.17},
URN = {urn:nbn:de:0030-drops-261543},
doi = {10.4230/DARTS.12.1.17},
annote = {Keywords: Parsing, Pratt Parsing, Recursive Descent, Extensible Syntax, Artifact}
}
Document
Artifact
Compositional Design, Implementation, and Verification of Swarms (Artifact)
Abstract
This is the companion artifact of the paper titled "Compositional Design, Implementation, and Verification of Swarms" (ECOOP'26). This artifact contains an extension of the open-source Actyx toolkit that implements the theoretical results in the paper. It also includes scripts to reproduce all experiments and claims in Section 6 of the paper, as well as documentation on the usage of our extended Actyx toolkit via various examples.
Cite as
Lucas Clorius, Florian Furbach, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional Design, Implementation, and Verification of Swarms (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 18:1-18:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{clorius_et_al:DARTS.12.1.18,
author = {Clorius, Lucas and Furbach, Florian and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
title = {{Compositional Design, Implementation, and Verification of Swarms (Artifact)}},
pages = {18:1--18:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Clorius, Lucas and Furbach, Florian and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.18},
URN = {urn:nbn:de:0030-drops-261559},
doi = {10.4230/DARTS.12.1.18},
annote = {Keywords: Swarms, Swarm Protocols, Concurrency, Distributed Coordination, Local-first Software, Behavioural Types, Publish-Subscribe, Asynchronous Communication}
}
Document
Artifact
Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-browser Cryptomining (Artifact)
Abstract
This artifact contains several supporting materials to the paper "Proof-of-Theft: Dynamic Graph-based Fingerprinting of In-browser Cryptomining". We provide code from our experiments implementing the analysis and detection algorithms described in the paper, along with a dataset of collected Wasm binaries, obfuscated Wasm binaries, data-flow graphs, and image rendering of data-flow graphs. The reader will find instructions and materials to reproduce our experiments, and an overview of how to apply our experimental process to other software.
Cite as
Tanapoom Sermchaiwong and Jiasi Shen. Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-browser Cryptomining (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 19:1-19:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{sermchaiwong_et_al:DARTS.12.1.19,
author = {Sermchaiwong, Tanapoom and Shen, Jiasi},
title = {{Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-browser Cryptomining (Artifact)}},
pages = {19:1--19:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Sermchaiwong, Tanapoom and Shen, Jiasi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.19},
URN = {urn:nbn:de:0030-drops-261569},
doi = {10.4230/DARTS.12.1.19},
annote = {Keywords: software security, cryptocurrency, malware detection, dynamic analysis, data-flow graph}
}
Document
Artifact
Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability (Artifact)
Abstract
Our related paper presents TnFix, a CFL (context-free language)-reachability-based technique for mitigating over-tainting in IFDS taint analysis. The approach addresses a common source of imprecision introduced by k-limiting: it prunes spurious access paths by checking candidate field sequences against per-object DFAs (deterministic finite automata). To build these DFAs, TnFix first solves a lightweight, field-sensitive CFL-reachability problem to construct a Field Points-to Graph (FPG) that integrates flows from taint sources and library summaries, and then transforms the FPG into object-specific DFAs used during analysis to reject infeasible field-access sequences.
This artifact bundles the implementation of TnFix (including field-sensitive CFL-reachability solving, per-object DFA construction, and DFA-based filtering), together with the evaluation harness used in the paper. It provides scripts to run TnFix and FlowDroid under identical settings and to reproduce the reported performance and precision results on the Android app set used in our evaluation.
Cite as
Yujiang Gui, Yonggang Tao, and Jingling Xue. Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 20:1-20:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{gui_et_al:DARTS.12.1.20,
author = {Gui, Yujiang and Tao, Yonggang and Xue, Jingling},
title = {{Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability (Artifact)}},
pages = {20:1--20:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Gui, Yujiang and Tao, Yonggang and Xue, Jingling},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.20},
URN = {urn:nbn:de:0030-drops-261573},
doi = {10.4230/DARTS.12.1.20},
annote = {Keywords: Taint Analysis, CFL-Reachability, Access Path, Field Sensitivity, Pointer Analysis.}
}
Document
Artifact
Verifying Wait-Freedom for Concurrent Higher-Order Programs (Artifact)
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 extend Lawyer with a novel adequacy theorem that proves that programs which are proven correct in the Lawyer logic against a specification in this aforementioned specification pattern are wait-free. Proving wait-freedom requires us to show that all calls made to operations by any arbitrary client terminate. Thus, as part of formally proving wait-freedom, i.e., as part of the proof of 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 higher-order functions such as the 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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{namakonov_et_al:DARTS.12.1.21,
author = {Namakonov, Egor and Birkedal, Lars and Timany, Amin},
title = {{Verifying Wait-Freedom for Concurrent Higher-Order Programs (Artifact)}},
pages = {21:1--21:8},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Namakonov, Egor and Birkedal, Lars and Timany, Amin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.21},
URN = {urn:nbn:de:0030-drops-261581},
doi = {10.4230/DARTS.12.1.21},
annote = {Keywords: separation logic, higher-order logic, concurrency, formal verification}
}
Document
Artifact
Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact)
Abstract
The companion paper proposes a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. The model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. A toolchain supports formal model validation, Solidity code generation (extensible to other smart contract languages), and automated test synthesis. Although targeting blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. The expressiveness and practicality of the approach are demonstrated through modelling and realising coordination patterns in smart contracts.
This artifact accompanies our paper [Elvis Konjoh Selabi et al., 2026]. It provides a toolchain for generating smart contract code from EDAM (Extended Data-Aware Machines) specifications. The artifact includes the complete source code, a Docker image for easy deployment, pre-generated experiment data (generated code, automated tests, and mutation testing results), and reproduction scripts.
Cite as
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 22:1-22:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{konjohselabi_et_al:DARTS.12.1.22,
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 (Artifact)}},
pages = {22:1--22:9},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Konjoh Selabi, Elvis and Murgia, Maurizio and Ravara, Ant\'{o}nio and Tuosto, Emilio},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.22},
URN = {urn:nbn:de:0030-drops-261590},
doi = {10.4230/DARTS.12.1.22},
annote = {Keywords: Smart Contracts, Coordination Models, Formal Semantics, Role-Based Access, Decentralised Systems, Code Generation, Solidity, Verification}
}
Document
Artifact
Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)
Abstract
This artifact accompanies the paper "Ownership Refinement Types for Pointer Arithmetic and Nested Arrays." It provides nested_array_ConSORT, a tool for automated ownership type inference and refinement type checking for imperative programs with pointer arithmetic and nested arrays. The artifact includes the tool implementation, benchmark programs, evaluation scripts to reproduce the experimental results (Tables 1, 3, 4, and 5) from the paper, and a comparison baseline (Extended_ConSORT by Tanaka et al. [Tanaka et al., 2024]). The artifact is packaged as a Docker image with all dependencies pre-installed, supporting both x86_64 and ARM64 platforms.
Cite as
Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, and Atsushi Igarashi. Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{fujiwara_et_al:DARTS.12.1.23,
author = {Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
title = {{Ownership Refinement Types for Pointer Arithmetic and Nested Arrays (Artifact)}},
pages = {23:1--23:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Fujiwara, Yusuke and Matsushita, Yusuke and Suenaga, Kohei and Igarashi, Atsushi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.23},
URN = {urn:nbn:de:0030-drops-261603},
doi = {10.4230/DARTS.12.1.23},
annote = {Keywords: aliasing, fractional ownership, program verification, refinement types, type systems}
}
Document
Artifact
Vardalith: Hybrid Detection of Persistent Memory Concurrency Bugs (Artifact)
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 (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 24:1-24:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Article{goncalves_et_al:DARTS.12.1.24,
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 (Artifact)}},
pages = {24:1--24:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2026},
volume = {12},
number = {1},
editor = {Gon\c{c}alves, Jo\~{a}o and Fragoso Santos, Jos\'{e} and Rodrigues, Rodrigo and Matos, Miguel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.24},
URN = {urn:nbn:de:0030-drops-261619},
doi = {10.4230/DARTS.12.1.24},
annote = {Keywords: persistent memory, concurrency, crash consistency}
}