Issue
DARTS, Volume 11, Issue 2
Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)
-
Part of:
Volume:
DARTS, Volume 11 (ECRTS 2025)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2025-06-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts11
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
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 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{evenmendoza_et_al:DARTS.11.2.0,
author = {Even-Mendoza, Karine and Monat, Rapha\"{e}l 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 = {2025},
volume = {11},
number = {2},
editor = {Even-Mendoza, Karine and Monat, Rapha\"{e}l 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.11.2.0},
URN = {urn:nbn:de:0030-drops-236599},
doi = {10.4230/DARTS.11.2.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
Ensuring Convergence and Invariants Without Coordination (Artifact)
Abstract
Our related paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. We implemented the core of the No-Op replication protocol in VeriFx [De Porre et al., 2023], a programming language for RDTs with automated proof capabilities. Alongside the algorithm implementation, we developed formal proofs to automatically verify the algorithm’s correctness properties when applied to specific data types or application implementations.
This artifact bundles the implementation of the No-Op framework, various CRDTs [Marc Shapiro et al., 2011], and an eBay-like auction system akin to the RUBiS system [Emmanuel Cecchet et al., 2002] described in Section 5 of the paper. The artifact also provides a Dockerfile that can be used to reproduce the verification results (Section 4 of the paper).
Cite as
Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{borrego_et_al:DARTS.11.2.1,
author = {Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
title = {{Ensuring Convergence and Invariants Without Coordination (Artifact)}},
pages = {1:1--1:7},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.1},
URN = {urn:nbn:de:0030-drops-233447},
doi = {10.4230/DARTS.11.2.1},
annote = {Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}
Document
Artifact
Bottom-Up Synthesis of Memory Mutations with Separation Logic (Artifact)
Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets.
We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction.
We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as
Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{ferdowsi_et_al:DARTS.11.2.2,
author = {Ferdowsi, Kasra and Peleg, Hila},
title = {{Bottom-Up Synthesis of Memory Mutations with Separation Logic (Artifact)}},
pages = {2:1--2:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Ferdowsi, Kasra and Peleg, Hila},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.2},
URN = {urn:nbn:de:0030-drops-233455},
doi = {10.4230/DARTS.11.2.2},
annote = {Keywords: Program synthesis, observational equivalence}
}
Document
Artifact
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)
Abstract
Session types offer a type-based approach to describing the message exchange protocols between participants in communication-based systems. Initially, they were introduced in a binary setting, specifying communication patterns between two components. With the advent of multiparty session types (MPST), the typing discipline was extended to arbitrarily many components. In MPST, communication patterns are given in terms of global types, an Alice-Bob notation that gives a global view of how components interact. A central theorem of MPST is subject reduction: a well-typed system remains well-typed after reduction. The literature contains some formulations of MPST with proofs of subject reduction that have later been shown to be incorrect. In this paper, we show that the subject reduction proof of the original formulation of MPST by Honda et al. contains some flaws. Additionally, we provide a restriction to the theory and show that, for this fragment, subject reduction does indeed hold. Finally, we use subject reduction to show that well-typed processes never go wrong. All of our proofs are mechanised using the Coq proof assistant.
This artifact accompanies our paper [Dawit Tirore et al., 2025]. It contains the Coq mechanisation of the theory described therein.
Cite as
Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{tirore_et_al:DARTS.11.2.3,
author = {Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
title = {{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)}},
pages = {3:1--3:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.3},
URN = {urn:nbn:de:0030-drops-233467},
doi = {10.4230/DARTS.11.2.3},
annote = {Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
Artifact
Contract Systems Need Domain-Specific Notations (Artifact)
Abstract
Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, the related article proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.
Cite as
Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{moy_et_al:DARTS.11.2.4,
author = {Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
title = {{Contract Systems Need Domain-Specific Notations (Artifact)}},
pages = {4:1--4:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.4},
URN = {urn:nbn:de:0030-drops-233472},
doi = {10.4230/DARTS.11.2.4},
annote = {Keywords: software contracts, domain-specific languages}
}
Document
Artifact
Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact)
Abstract
This artifact accompanies the submission entitled "Compositional Static Value Analysis for Higher-Order Numerical Programs". 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é. Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{valnet_et_al:DARTS.11.2.5,
author = {Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
title = {{Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact)}},
pages = {5:1--5:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
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.11.2.5},
URN = {urn:nbn:de:0030-drops-233481},
doi = {10.4230/DARTS.11.2.5},
annote = {Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
Artifact
Declarative Dynamic Object Reclassification (Artifact)
Abstract
This artifact contains the GreenhouseDT API, a backend API for the GreenhouseDT system, which implements the declarative dynamic object reclassification in the SMOL language, as specified and described in the paper "Declarative Dynamic Object Reclassification". It also contains a Python to reproduce the results of the paper. This artifact description describes how the artifact is structured, as well as how to build and run it.
Cite as
Riccardo Sieve, Eduard Kamburjan, Ferruccio Damiani, and Einar Broch Johnsen. Declarative Dynamic Object Reclassification (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 6:1-6:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{sieve_et_al:DARTS.11.2.6,
author = {Sieve, Riccardo and Kamburjan, Eduard and Damiani, Ferruccio and Johnsen, Einar Broch},
title = {{Declarative Dynamic Object Reclassification (Artifact)}},
pages = {6:1--6:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Sieve, Riccardo and Kamburjan, Eduard and Damiani, Ferruccio and Johnsen, Einar Broch},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.6},
URN = {urn:nbn:de:0030-drops-233496},
doi = {10.4230/DARTS.11.2.6},
annote = {Keywords: Dynamic Object Reclassification, Dynamic Software Updates, Featherweight Java, Knowledge Bases, Semantic Reflection, Type Soundness}
}
Document
Artifact
Practical Type-Based Taint Checking and Inference (Artifact)
Abstract
We present a containerized framework for the paper Practical Type-Based Taint Checking and Inference. Packed as a Docker image, the artifact bundles our novel inference engine alongside CodeQL and P/Taint analyses, together with precomputed results and scripts to reproduce five core experimental tables: benchmark characteristics, soundness on labeled issues, precision/recall on real‐world projects, runtime comparisons, and annotation ablation studies. By unifying checking and inference in a portable setup, this artifact enables straightforward validation of our paper’s claims.
Cite as
Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi. Practical Type-Based Taint Checking and Inference (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{karimipour_et_al:DARTS.11.2.7,
author = {Karimipour, Nima and Das, Kanak and Sridharan, Manu and Hassanshahi, Behnaz},
title = {{Practical Type-Based Taint Checking and Inference (Artifact)}},
pages = {7:1--7:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Karimipour, Nima and Das, Kanak and Sridharan, Manu and Hassanshahi, Behnaz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.7},
URN = {urn:nbn:de:0030-drops-233509},
doi = {10.4230/DARTS.11.2.7},
annote = {Keywords: Static analysis, Taint Analysis, Pluggable type systems, Security, Inference}
}
Document
Artifact
A Theory of (Linear-Time) Timed Monitors (Artifact)
Abstract
We provide an OCaml implementation of the logics MTL and T^lin, as well as monitors. Our artefact includes a compiler that translates T^lin formulae into monitors. The generation of a monitor M from some formula ϕ is decorated with a warning whenever ϕ is not in the syntax of the maximally-expressive monitorable fragment. The resulting monitors being reactive and deterministic, we also implement their semantics, and provide further a pseudo-monitoring prototype where the monitor incrementally consumes an infinite timed word and reaches a verdict whenever possible. For convenience, for users that prefer to use MTL (bearing in mind the loss of expressivity), we also provide a compiler from MTL to T^lin.
Cite as
Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{amara_et_al:DARTS.11.2.8,
author = {Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
title = {{A Theory of (Linear-Time) Timed Monitors (Artifact)}},
pages = {8:1--8:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.8},
URN = {urn:nbn:de:0030-drops-233517},
doi = {10.4230/DARTS.11.2.8},
annote = {Keywords: Timed logics, Runtime verification, Monitorability}
}
Document
Artifact
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact)
Abstract
This artifact is a companion to the paper "Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness". It contains the Rocq formalisation of the RISL program logic, the RUXtBelt semantic model and the inadequacy theorem of RUXt. It also contains the OCaml prototype for RUXt, along with the case studies discussed in the paper.
Cite as
Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{carrott_et_al:DARTS.11.2.9,
author = {Carrott, Pedro and Ayoun, Sacha-\'{E}lie and Raad, Azalea},
title = {{Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact)}},
pages = {9:1--9:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Carrott, Pedro and Ayoun, Sacha-\'{E}lie and Raad, Azalea},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.9},
URN = {urn:nbn:de:0030-drops-233529},
doi = {10.4230/DARTS.11.2.9},
annote = {Keywords: Rust, bug detection, static analysis, program logics, under-approximation}
}
Document
Artifact
The Algebra of Patterns - Rocq Proofs (Artifact)
Abstract
This artifact provides Rocq proofs for all the theorems of section 3 of the paper The Algebra of Patterns. Concretely, these are theorems 3, 4, 7, 8, 9, 10, 11, 12, 13 and 15.
Cite as
David Binder and Lean Ermantraut. The Algebra of Patterns - Rocq Proofs (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{binder_et_al:DARTS.11.2.10,
author = {Binder, David and Ermantraut, Lean},
title = {{The Algebra of Patterns - Rocq Proofs (Artifact)}},
pages = {10:1--10:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Binder, David and Ermantraut, Lean},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.10},
URN = {urn:nbn:de:0030-drops-233531},
doi = {10.4230/DARTS.11.2.10},
annote = {Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}
Document
Artifact
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees (Artifact)
Abstract
The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch and bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that need to be split, it explores the space of these sub-problems in a naive "first-come-first-served" manner, thereby suffering from an issue of inefficiency in reaching a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problem and so will not lead to a performance degradation. Specifically, Oliva has two variants, including Oliva^GR, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and Oliva^SA, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10.
Cite as
Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 11:1-11:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{zhang_et_al:DARTS.11.2.11,
author = {Zhang, Guanqin and Fukuda, Kota and Zhang, Zhenya and Bandara, H.M.N. Dilum and Chen, Shiping and Zhao, Jianjun and Sui, Yulei},
title = {{Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees (Artifact)}},
pages = {11:1--11:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Zhang, Guanqin and Fukuda, Kota and Zhang, Zhenya and Bandara, H.M.N. Dilum and Chen, Shiping and Zhao, Jianjun and Sui, Yulei},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.11},
URN = {urn:nbn:de:0030-drops-233545},
doi = {10.4230/DARTS.11.2.11},
annote = {Keywords: neural network verification, branch and bound, counterexample potentiality, simulated annealing, stochastic optimization}
}
Document
Artifact
Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact)
Abstract
This artifact supports the paper “Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design.” It provides an implementation of Cope and Drag (CnD), a lightweight diagramming language grounded in cognitive principles and a corpus analysis of existing visualizations. CnD enables users to define diagrams using a small set of orthogonal primitives that capture essential domain structure while avoiding the complexity of writing full visualization programs. The artifact allows exploration of CnD’s implementation and reproduction of claims made in the accompanying paper.
Cite as
Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{prasad_et_al:DARTS.11.2.12,
author = {Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
title = {{Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact)}},
pages = {12:1--12:11},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Prasad, Siddhartha and Greenman, Ben and Nelson, Tim 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.11.2.12},
URN = {urn:nbn:de:0030-drops-233552},
doi = {10.4230/DARTS.11.2.12},
annote = {Keywords: formal methods, diagramming, visualization, language design}
}
Document
Artifact
Incremental Computing by Differential Execution (Artifact)
Abstract
This artifact supports the paper titled "Incremental Computing by Differential Execution" accepted at ECOOP 2025. It provides a mechanized formalization in Rocq of the differential semantics and optimizations presented in the paper, along with a reference implementation of the differential interpreter in Scala. The artifact includes the Bellman-Ford benchmark used for the performance evaluation in Section 7. Both components are packaged as Docker images for ease of use and reproducibility, enabling verification of all claims made in the paper.
Cite as
Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 13:1-13:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{kumar_et_al:DARTS.11.2.13,
author = {Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
title = {{Incremental Computing by Differential Execution (Artifact)}},
pages = {13:1--13:8},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Kumar, Prashant and Pacak, Andr\'{e} 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.11.2.13},
URN = {urn:nbn:de:0030-drops-233564},
doi = {10.4230/DARTS.11.2.13},
annote = {Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics}
}
Document
Artifact
WebGlitch: A Randomised Testing Tool for the WebGPU API (Artifact)
Abstract
We present the software artifact that accompanies our paper on WebGlitch, a new tool for fuzz testing WebGPU implementations, along with detailed instructions for its use. The artifact consists of a Docker image containing the complete setup to run WebGlitch on two WebGPU implementations, Dawn and wgpu, via Node.js and Deno, respectively. This image allows users to reproduce the throughput and coverage experiments described in the paper, and provides a playground for generating WebGPU programs with WebGlitch and testing different WebGPU implementations. We also include the full source code for WebGlitch for transparency. We hope this artifact will support future research in testing the WebGPU ecosystem and API fuzzing more broadly.
Cite as
Matthew K. L. Wong and Alastair F. Donaldson. WebGlitch: A Randomised Testing Tool for the WebGPU API (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 14:1-14:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{wong_et_al:DARTS.11.2.14,
author = {Wong, Matthew K. L. and Donaldson, Alastair F.},
title = {{WebGlitch: A Randomised Testing Tool for the WebGPU API (Artifact)}},
pages = {14:1--14:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Wong, Matthew K. L. and Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.14},
URN = {urn:nbn:de:0030-drops-233578},
doi = {10.4230/DARTS.11.2.14},
annote = {Keywords: Fuzzing, WebGPU, WGSL, API, shaders, artifact}
}
Document
Artifact
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact)
Abstract
Static analysis by means of abstract interpretation is a tool of choice for proving absence of some classes of errors, typically undefined behaviors in code, in a sound way. However, static analysis tools are hardly integrated in CI/CD processes. One of the main reasons is that they are still time- and memory-expensive to apply after every single patch when developing a program. For solving this issue, incremental static analysis helps developers quickly obtain analysis results after making changes to a program. However, existing approaches are often not guaranteed to be sound, limited to specific analyses, or tied to specific tools. This limits their generalizability and applicability in practice, especially for large and critical software. In this paper, we propose a generic, sound approach to incremental static analysis that is applicable to any abstract interpreter. Our approach leverages the similarity between two versions of a program to soundly reuse previously computed analysis results. We introduce novel methods for summarizing functions and reusing loop invariants. They significantly reduce the cost of reanalysis, while maintaining soundness and a high level of precision. We have formalized our approach, proved it sound, implemented it in Eva, the abstract interpreter of Frama-C, and evaluated it on a set of real-world commits of open-source programs.
Cite as
Mamy Razafintsialonina, David Bühler, and Valentin Perrelle. Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{razafintsialonina_et_al:DARTS.11.2.15,
author = {Razafintsialonina, Mamy and B\"{u}hler, David and Perrelle, Valentin},
title = {{Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact)}},
pages = {15:1--15:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Razafintsialonina, Mamy and B\"{u}hler, David and Perrelle, Valentin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.15},
URN = {urn:nbn:de:0030-drops-233586},
doi = {10.4230/DARTS.11.2.15},
annote = {Keywords: Abstract Interpretation, Static Analysis, Incremental Analysis}
}
Document
Artifact
A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework (Artifact)
Abstract
Meta-compiler frameworks, such as RPython and Graal/Truffle, generate high-performance virtual machines (VMs) from interpreter definitions. Although they generate VMs with high-quality just-in-time (JIT) compilers, they still lack an important feature that dedicated VMs (i.e., VMs that are developed for specific languages) have, namely multi-tier compilation. Multi-tier compilation uses light-weight compilers at early stages and highly optimizing compilers at later stages in order to balance between compilation overheads and code quality.
We propose a novel approach to enabling multi-tier compilation in the VMs generated by a meta-compiler framework. Instead of extending the JIT compiler backend of the framework, our approach drives an existing (heavyweight) compiler backend in the framework to quickly generate unoptimized native code by merely embedding directives and compile-time operations into interpreter definitions.
As a validation of the approach, we developed 2SOM, a Simple Object Machine with a two-tier JIT compiler based on RPython. 2SOM first applies the tier-1 threaded code generator that is generated by our proposed technique, then, to the loops that exceed a threshold, applies the tier-2 tracing JIT compiler that is generated by the original RPython framework. Our performance evaluation that runs a program with a realistic workload showed that 2SOM improved, when compared against an RPython-based VM, warm-up performance by 15%, with merely a 5% reduction in peak performance.
Cite as
Yusuke Izawa, Hidehiko Masuhara, and Carl Friedrich Bolz-Tereick. A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 16:1-16:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{izawa_et_al:DARTS.11.2.16,
author = {Izawa, Yusuke and Masuhara, Hidehiko and Bolz-Tereick, Carl Friedrich},
title = {{A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework (Artifact)}},
pages = {16:1--16:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Izawa, Yusuke and Masuhara, Hidehiko and Bolz-Tereick, Carl Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.16},
URN = {urn:nbn:de:0030-drops-233590},
doi = {10.4230/DARTS.11.2.16},
annote = {Keywords: virtual machine, JIT compiler, multi-tier JIT compiler, meta-tracing JIT compiler, RPython}
}
Document
Artifact
GSOHC: Global Synchronization Optimization for Heterogeneous Computing (Artifact)
Abstract
The use of heterogeneous systems has become widespread and popular in the past decade with more than one type of processor, such as CPUs, GPUs (Graphics Processing Units), and FPGAs (Field Programmable Gate Arrays) etc. A wide range of applications use both CPU and GPU to leverage the benefits of their unique features and strengths. Therefore, collaborative computation between CPU and GPU is essential to achieve high program performance. However, poorly placed global synchronization barriers and synchronous memory transfers are the main bottlenecks to enhanced program performance, preventing CPU and GPU computations from overlapping.
Based on this observation, we propose a new optimization technique called hetero-sync motion that can relocate such barrier instructions to new locations, resulting in improved performance in CPU-GPU heterogeneous programs. Further, we propose GSOHC, a compiler analysis and optimization framework that automatically finds opportunities for hetero-sync motion in the input program and then performs code transformation to apply the optimization. Our static analysis is a context-sensitive, flow-sensitive inter-procedural data-flow analysis with three phases to identify the optimization opportunities precisely. We have implemented GSOHC using LLVM/Clang infrastructure. On A4000, P100 and A100 GPUs, our optimization achieves up to 1.8x, up to 1.9x and up to 1.9x speedups over baseline, respectively.
Cite as
Soumik Kumar Basu and Jyothi Vedurada. GSOHC: Global Synchronization Optimization for Heterogeneous Computing (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 17:1-17:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{kumarbasu_et_al:DARTS.11.2.17,
author = {Kumar Basu, Soumik and Vedurada, Jyothi},
title = {{GSOHC: Global Synchronization Optimization for Heterogeneous Computing (Artifact)}},
pages = {17:1--17:7},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Kumar Basu, Soumik and Vedurada, Jyothi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.17},
URN = {urn:nbn:de:0030-drops-233603},
doi = {10.4230/DARTS.11.2.17},
annote = {Keywords: Static Analysis, Synchronization, CPU-GPU, Heterogeneous Computing, Parallelization}
}
Document
Artifact
Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact)
Abstract
This is the accompanying artifact for the ECOOP 25' paper "Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions".
Cite as
Jacqueline L. Mitchell and Chao Wang. Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 18:1-18:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{mitchell_et_al:DARTS.11.2.18,
author = {Mitchell, Jacqueline L. and Wang, Chao},
title = {{Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact)}},
pages = {18:1--18:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2025},
volume = {11},
number = {2},
editor = {Mitchell, Jacqueline L. 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.11.2.18},
URN = {urn:nbn:de:0030-drops-233619},
doi = {10.4230/DARTS.11.2.18},
annote = {Keywords: Abstract interpretation, side-channel, leakage quantification, cache}
}