Volume
LIPIcs, Volume 333
39th European Conference on Object-Oriented Programming (ECOOP 2025)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
ECOOP 2025, June 30 to July 2, 2025, Bergen, NorwayEditors
Publication Details
- published at: 2025-06-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-373-7
- DBLP: db/conf/ecoop/ecoop2025
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
Complete Volume
LIPIcs, Volume 333, ECOOP 2025, Complete Volume
Abstract
LIPIcs, Volume 333, ECOOP 2025, Complete Volume
Cite as
39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 1-1202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{aldrich_et_al:LIPIcs.ECOOP.2025,
title = {{LIPIcs, Volume 333, ECOOP 2025, Complete Volume}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {1--1202},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025},
URN = {urn:nbn:de:0030-drops-236580},
doi = {10.4230/LIPIcs.ECOOP.2025},
annote = {Keywords: LIPIcs, Volume 333, ECOOP 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{aldrich_et_al:LIPIcs.ECOOP.2025.0,
author = {Aldrich, Jonathan and Silva, Alexandra},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.0},
URN = {urn:nbn:de:0030-drops-236553},
doi = {10.4230/LIPIcs.ECOOP.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
A Theory of (Linear-Time) Timed Monitors
Abstract
Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic.
Cite as
Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{amara_et_al:LIPIcs.ECOOP.2025.1,
author = {Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
title = {{A Theory of (Linear-Time) Timed Monitors}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {1:1--1:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.1},
URN = {urn:nbn:de:0030-drops-232930},
doi = {10.4230/LIPIcs.ECOOP.2025.1},
annote = {Keywords: Timed logics, Runtime Verification, Monitorability}
}
Document
The Algebra of Patterns
Abstract
Pattern matching is a popular feature in functional, imperative and object-oriented programming languages. Language designers should therefore invest effort in a good design for pattern matching. Most languages choose a first-match semantics for pattern matching; that is, clauses are tried in the order in which they appear in the program until the first one matches. As a consequence, the order in which the clauses appear cannot be arbitrarily changed, which results in a less declarative programming model. The declarative alternative to this is an order-independent semantics for pattern matching, which is not implemented in most programming languages since it requires more verbose patterns. The reason for this verbosity is that the syntax of patterns is usually not expressive enough to express the complement of a pattern. In this paper, we show a principled way to make order-independent pattern matching practical. Our solution consists of two parts: First, we introduce a boolean algebra of patterns which can express the complement of a pattern. Second, we introduce default clauses to pattern matches. These default clauses capture the essential idea of a fallthrough case without sacrificing the property of order-independence.
Cite as
David Binder and Lean Ermantraut. The Algebra of Patterns. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{binder_et_al:LIPIcs.ECOOP.2025.2,
author = {Binder, David and Ermantraut, Lean},
title = {{The Algebra of Patterns}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {2:1--2:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.2},
URN = {urn:nbn:de:0030-drops-232959},
doi = {10.4230/LIPIcs.ECOOP.2025.2},
annote = {Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}
Document
Pydrofoil: Accelerating Sail-Based Instruction Set Simulators
Abstract
We present Pydrofoil, a multi-stage compiler that generates instruction set simulators (ISSs) from processor instruction set architectures (ISAs) expressed in the high-level, verification-oriented ISA specification language Sail. Pydrofoil achieves a > 230× speedup over the C-based ISS generated by Sail on our benchmarks, thanks to the following insights. (i) An ISS is effectively an interpreter loop, and tracing just-in-time (JIT) compilers have proven effective at accelerating those, albeit mostly for dynamically typed languages. (ii) ISS workloads are highly atypical, dominated by intensive bit manipulation operations. Conventional compiler optimisations for general-purpose programming languages have limited impact for speeding up such workloads. We develop suitable domain-specific optimisations. (iii) Neither tracing JIT compilers, nor ahead-of-time (AOT) compilation alone, even with domain-specific optimisations, suffice for the generation of performant ISSs. Pydrofoil therefore implements a hybrid approach, pairing an AOT compiler with a tracing JIT built on the meta-tracing PyPy framework. AOT and JIT use domain-specific optimisations. Our benchmarks demonstrate that combining AOT and JIT compilers provides significantly greater performance gains than using either compiler alone.
Cite as
Carl Friedrich Bolz-Tereick, Luke Panayi, Ferdia McKeogh, Tom Spink, and Martin Berger. Pydrofoil: Accelerating Sail-Based Instruction Set Simulators. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 3:1-3:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bolztereick_et_al:LIPIcs.ECOOP.2025.3,
author = {Bolz-Tereick, Carl Friedrich and Panayi, Luke and McKeogh, Ferdia and Spink, Tom and Berger, Martin},
title = {{Pydrofoil: Accelerating Sail-Based Instruction Set Simulators}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {3:1--3:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.3},
URN = {urn:nbn:de:0030-drops-232962},
doi = {10.4230/LIPIcs.ECOOP.2025.3},
annote = {Keywords: Instruction set architecture, processor, domain-specific language, just-in-time compilation, meta-tracing}
}
Document
Ensuring Convergence and Invariants Without Coordination
Abstract
The CAP theorem demonstrates a trade-off between consistency and availability (and, by extension, latency) in systems where network partitions are unavoidable, such as in cloud computing and local-first software. While adopting weak consistency can preserve availability, it may result in inconsistencies that compromise application correctness. Replicated data types provide a principled, coordination-free approach to guarantee convergence but do not consider application invariants. Existing methods for maintaining invariants in replicated systems either rely on coordination - undermining the benefits of weak consistency - or suffer from limited applicability. This paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. The core idea of the No-Op approach is to resolve conflicts among concurrent operations by prioritising one operation over the other according to programmer-defined conflict resolution policies. This prioritisation transforms the less-preferred operation into a no-side-effect operation, ensuring conflict-free execution. We formalise the model underlying the No-Op framework and introduce a replication protocol built upon it, accompanied by a formal proof of correctness for both the framework and the protocol. Furthermore, we demonstrate the framework’s applicability by showcasing the design of widely used replicated data types and the preservation of a wide range of application invariants.
Cite as
Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{borrego_et_al:LIPIcs.ECOOP.2025.4,
author = {Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
title = {{Ensuring Convergence and Invariants Without Coordination}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {4:1--4:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.4},
URN = {urn:nbn:de:0030-drops-232978},
doi = {10.4230/LIPIcs.ECOOP.2025.4},
annote = {Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}
Document
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness
Abstract
Rust is a modern programming language marrying the best of language design by offering fine-grained control over system resources (thus enabling efficient implementations), while simultaneously ensuring memory safety and data-race freedom. However, ensuring type safety in internally unsafe libraries remains an important and non-trivial challenge, where unsafe features enable low-level control but can introduce undefined behaviour (UB). Existing works on reasoning about unsafe code either use verification techniques to show correctness (i.e. safety, useful only when the unsafe code is indeed correct), or use bug detection techniques to show incorrectness (i.e. unsafety) but fail to do so automatically (to avoid developer burden), compositionally (to support libraries without a main function), soundly (without false positives) and generally (rather than applying to specific patterns).
We close this gap by developing RUXt, a fully automatic, compositional bug detection technique for detecting UB in internally unsafe Rust libraries with a formal inadequacy theorem (formalised and proven in Rocq) providing a no-false-positives guarantee. RUXt leverages the Rust type system to under-approximate the set of safe values for user-defined types and detect safety violations without requiring manual annotations by the user. By encoding well-typed values in Rust as separation logic assertions, RUXt enables compositional reasoning about types to refute unsound type signatures and detect UB. The inadequacy theorem of RUXt ensures that each UB detected by RUXt in an internally unsafe library is a true safety violation that can be triggered by a safe program, i.e. one that solely interacts with the safe API of the library. To this end, when RUXt identifies a UB, it additionally produces a safe program witnessing the UB. In addition, we develop a prototype implementation in OCaml that can analyse programs written in a small model of Rust, and apply it to several case studies, showcasing its ability to detect true safety violations.
Cite as
Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{carrott_et_al:LIPIcs.ECOOP.2025.5,
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}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {5:1--5:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.5},
URN = {urn:nbn:de:0030-drops-232988},
doi = {10.4230/LIPIcs.ECOOP.2025.5},
annote = {Keywords: Rust, bug detection, static analysis, program logics, under-approximation}
}
Document
Detecting Functionality-Specific Vulnerabilities via Retrieving Individual Functionality-Equivalent APIs in Open-Source Repositories
Abstract
Functionality-specific vulnerabilities, which mainly occur in Application Programming Interfaces (APIs) with specific functionalities, are crucial for software developers to detect and avoid. When detecting individual functionality-specific vulnerabilities, the existing two categories of approaches are ineffective because they consider only the API bodies and are unable to handle diverse implementations of functionality-equivalent APIs. To effectively detect functionality-specific vulnerabilities, we propose APISS, the first approach to utilize API doc strings and signatures instead of API bodies. APISS first retrieves functionality-equivalent APIs for APIs with existing vulnerabilities and then migrates Proof-of-Concepts (PoCs) of the existing vulnerabilities for newly detected vulnerable APIs. To retrieve functionality-equivalent APIs, we leverage a Large Language Model for API embedding to improve the accuracy and address the effectiveness and scalability issues suffered by the existing approaches. To migrate PoCs of the existing vulnerabilities for newly detected vulnerable APIs, we design a semi-automatic schema to substantially reduce manual costs. We conduct a comprehensive evaluation to empirically compare APISS with four state-of-the-art approaches of detecting vulnerabilities and two state-of-the-art approaches of retrieving functionality-equivalent APIs. The evaluation subjects include 180 widely used Java repositories using 10 existing vulnerabilities, along with their PoCs. The results show that APISS effectively retrieves functionality-equivalent APIs, achieving a Top-1 Accuracy of 0.81 while the best of the baselines under comparison achieves only 0.55. APISS is highly efficient: the manual costs are within 10 minutes per vulnerability and the end-to-end runtime overhead of testing one candidate API is less than 2 hours. APISS detects 179 new vulnerabilities and receives 60 new CVE IDs, bringing high value to security practice.
Cite as
Tianyu Chen, Zeyu Wang, Lin Li, Ding Li, Zongyang Li, Xiaoning Chang, Pan Bian, Guangtai Liang, Qianxiang Wang, and Tao Xie. Detecting Functionality-Specific Vulnerabilities via Retrieving Individual Functionality-Equivalent APIs in Open-Source Repositories. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.ECOOP.2025.6,
author = {Chen, Tianyu and Wang, Zeyu and Li, Lin and Li, Ding and Li, Zongyang and Chang, Xiaoning and Bian, Pan and Liang, Guangtai and Wang, Qianxiang and Xie, Tao},
title = {{Detecting Functionality-Specific Vulnerabilities via Retrieving Individual Functionality-Equivalent APIs in Open-Source Repositories}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {6:1--6:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.6},
URN = {urn:nbn:de:0030-drops-232999},
doi = {10.4230/LIPIcs.ECOOP.2025.6},
annote = {Keywords: Application Security, Vulnerability Detection, Large Language Model}
}
Document
Monadic Type-And-Effect Soundness
Abstract
We introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usual in the non-monadic case, we can express progress and subject reduction, and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects, equipped with an expressive type-and-effect system We provide proofs of progress and subject reduction, parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.
Cite as
Francesco Dagnino, Paola Giannini, and Elena Zucca. Monadic Type-And-Effect Soundness. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dagnino_et_al:LIPIcs.ECOOP.2025.7,
author = {Dagnino, Francesco and Giannini, Paola and Zucca, Elena},
title = {{Monadic Type-And-Effect Soundness}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {7:1--7:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.7},
URN = {urn:nbn:de:0030-drops-233009},
doi = {10.4230/LIPIcs.ECOOP.2025.7},
annote = {Keywords: Effects, monads, type soundness}
}
Document
An Effectful Object Calculus
Abstract
We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a recently introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.
Cite as
Francesco Dagnino, Paola Giannini, and Elena Zucca. An Effectful Object Calculus. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dagnino_et_al:LIPIcs.ECOOP.2025.8,
author = {Dagnino, Francesco and Giannini, Paola and Zucca, Elena},
title = {{An Effectful Object Calculus}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {8:1--8:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.8},
URN = {urn:nbn:de:0030-drops-233017},
doi = {10.4230/LIPIcs.ECOOP.2025.8},
annote = {Keywords: Object calculi, handlers, type-and-effect systems}
}
Document
Event Race Detection for Node.js Using Delay Injections
Abstract
Node.js is a widely used platform for building JavaScript server-side web applications, desktop applications, and software engineering tools. Its asynchronous execution model is essential for performance, but also gives rise to event races, which cause many subtle bugs that can be hard to detect and reproduce. Current solutions to expose such races are based on modifications of the source code of the Node.js system or on guided executions using complex happens-before modeling.
This paper presents a simpler and more effective approach called NACD that works by dynamically instrumenting core asynchronous operations in the Node.js runtime system to inject delays and thereby reveal event race bugs. It consists of a small, robust runtime instrumentation module implemented in JavaScript that is configured by a flexible JSON model of the essential parts of the Node.js API. Experimental results show that NACD can reproduce event race bugs with higher probability and fewer runs than state-of-the-art tools.
Cite as
Andre Takeshi Endo and Anders Møller. Event Race Detection for Node.js Using Delay Injections. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 9:1-9:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{endo_et_al:LIPIcs.ECOOP.2025.9,
author = {Endo, Andre Takeshi and M{\o}ller, Anders},
title = {{Event Race Detection for Node.js Using Delay Injections}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {9:1--9:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.9},
URN = {urn:nbn:de:0030-drops-233026},
doi = {10.4230/LIPIcs.ECOOP.2025.9},
annote = {Keywords: JavaScript, race conditions, flaky tests, event races, callback interleaving}
}
Document
Bottom-Up Synthesis of Memory Mutations with Separation Logic
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. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
author = {Ferdowsi, Kasra and Peleg, Hila},
title = {{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {10:1--10:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.10},
URN = {urn:nbn:de:0030-drops-233036},
doi = {10.4230/LIPIcs.ECOOP.2025.10},
annote = {Keywords: Program synthesis, observational equivalence}
}
Document
Contract Usage and Evolution in Android Mobile Applications
Abstract
Contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. Previous research has demonstrated the value of contracts in traditional software development. However, the adoption and impact of contracts in the context of mobile app development, particularly of Android apps, remain unexplored.
To address this, we present the first large-scale empirical study on the use of contracts in Android apps, written in Java or Kotlin. We consider contract elements divided into five categories: conditional runtime exceptions, APIs, annotations, assertions, and other. We analyzed 2,390 Android apps from the F-Droid repository and processed 52,977 KLOC to determine 1) how and to what extent contracts are used, 2) which language features are used to denote contracts, 3) how contract usage evolves from the first to the last version, and 4) whether contracts are used safely in the context of program evolution and inheritance. Our findings include: 1) although most apps do not specify contracts, annotation-based approaches are the most popular; 2) apps that use contracts continue to use them in later versions, but the number of methods increases at a higher rate than the number of contracts; and 3) there are potentially unsafe specification changes when apps evolve and in subtyping relationships, which indicates a lack of specification stability. Finally, we present a qualitative study that gathers challenges faced by practitioners when using contracts and that validates our recommendations.
Cite as
David R. Ferreira, Alexandra Mendes, João F. Ferreira, and Carolina Carreira. Contract Usage and Evolution in Android Mobile Applications. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 11:1-11:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ferreira_et_al:LIPIcs.ECOOP.2025.11,
author = {Ferreira, David R. and Mendes, Alexandra and Ferreira, Jo\~{a}o F. and Carreira, Carolina},
title = {{Contract Usage and Evolution in Android Mobile Applications}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {11:1--11:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.11},
URN = {urn:nbn:de:0030-drops-233041},
doi = {10.4230/LIPIcs.ECOOP.2025.11},
annote = {Keywords: Contracts, Design by Contract, DbC, Android, Java, Kotlin}
}
Document
Automatic Goal Clone Detection in Rocq
Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as
Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
author = {Ghanbari, Ali},
title = {{Automatic Goal Clone Detection in Rocq}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {12:1--12:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.12},
URN = {urn:nbn:de:0030-drops-233055},
doi = {10.4230/LIPIcs.ECOOP.2025.12},
annote = {Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
FuzzFlesh: Randomised Testing of Decompilers via Control Flow Graph-Based Program Generation
Abstract
Decompilation is the process of translating compiled code into high-level code. Control flow recovery is a challenging part of the process. "Misdecompilations" can occur, whereby the decompiled code does not accurately represent the semantics of the compiled code, despite it being syntactically valid. This is problematic because it can mislead users who are trying to reason about the program.
We present CFG-based program generation: a novel approach to randomised testing that aims to improve the control flow recovery of decompilers. CFG-based program generation involves randomly generating control flow graphs (CFGs) and paths through each graph. Inspired by prior work in the domain of GPU computing, (CFG, path) pairs are "fleshed" into test programs. Each program is decompiled and recompiled. The test oracle verifies whether the actual runtime path through the graph matches the expected path. Any difference in the execution paths after recompilation indicates a possible misdecompilation. A key benefit of this approach is that it is largely independent of the source and target languages in question because it is focused on control flow. The approach is therefore applicable to numerous decompilation settings. The trade-off resulting from the focus on control flow is that misdecompilation bugs that do not relate to control flow (e.g. bugs that involve specific arithmetic operations) are out of scope.
We have implemented this approach in FuzzFlesh, an open-source randomised testing tool. FuzzFlesh can be easily configured to target a variety of low-level languages and decompiler toolchains because most of the CFG and path generation process is language-independent. At present, FuzzFlesh supports testing decompilation of Java bytecode, .NET assembly and x86 machine code. In addition to program generation, FuzzFlesh also includes an automated test-case reducer that operates on the CFG rather than the low-level program, which means that it can be applied to any of the target languages.
We present a large experimental campaign applying FuzzFlesh to a variety of decompilers, leading to the discovery of 12 previously-unknown bugs across two language formats, six of which have been fixed. We present experiments comparing our generic FuzzFlesh tool to two state-of-the-art decompiler testing tools targeted at specific languages. As expected, the coverage our generic FuzzFlesh tool achieves on a given decompiler is lower than the coverage achieved by a tool specifically designed for the input format of that decompiler. However, due to its focus on control flow, FuzzFlesh is able to cover sections of control flow recovery code that the targeted tools cannot reach, and identify control flow related bugs that the targeted tools miss.
Cite as
Amber Gorzynski and Alastair F. Donaldson. FuzzFlesh: Randomised Testing of Decompilers via Control Flow Graph-Based Program Generation. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 13:1-13:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{gorzynski_et_al:LIPIcs.ECOOP.2025.13,
author = {Gorzynski, Amber and Donaldson, Alastair F.},
title = {{FuzzFlesh: Randomised Testing of Decompilers via Control Flow Graph-Based Program Generation}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {13:1--13:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.13},
URN = {urn:nbn:de:0030-drops-233062},
doi = {10.4230/LIPIcs.ECOOP.2025.13},
annote = {Keywords: Decompiler, Reverse Engineering, Control Flow, Software Testing, Fuzzing}
}
Document
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL
Abstract
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP’s intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable.
To make verification tractable, we develop a number of big-step rules that combine BIL’s existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.
Cite as
Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{griffin_et_al:LIPIcs.ECOOP.2025.14,
author = {Griffin, Matt and Dongol, Brijesh and Raad, Azalea},
title = {{IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {14:1--14:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.14},
URN = {urn:nbn:de:0030-drops-233070},
doi = {10.4230/LIPIcs.ECOOP.2025.14},
annote = {Keywords: Binary Analysis Platform, Isabelle/HOL, Hoare Logic, Incorrectness Logic}
}
Document
Spegion: Implicit and Non-Lexical Regions with Sized Allocations
Abstract
Region based memory management is a powerful tool designed with the goal of ensuring memory safety statically. The region calculus of Tofte and Talpin is a well known example of a region based system, which uses regions to manage memory in a stack-like fashion. However, the region calculus is lexically scoped and requires explicit annotation of memory regions, which can be cumbersome for the programmer. Other systems have addressed non-lexical regions, but these approaches typically require the use of a substructural type system to track the lifetimes of regions. We present Spegion, a language with implicit non-lexical regions, which provides these same memory safety guarantees for programs that go beyond using memory allocation in a stack-like manner. We are able to achieve this with a concise syntax, and without the use of substructural types, relying instead on an effect system to enforce constraints on region allocation and deallocation. These regions may be divided into sub-regions, i.e., Splittable rEgions, allowing fine grained control over memory allocation. Furthermore, Spegion permits sized allocations, where each value has an associated size which is used to ensure that regions are not over-allocated into. We present a type system for Spegion and prove it is type safe with respect to a small-step operational semantics.
Cite as
Jack Hughes, Michael Vollmer, and Mark Batty. Spegion: Implicit and Non-Lexical Regions with Sized Allocations. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hughes_et_al:LIPIcs.ECOOP.2025.15,
author = {Hughes, Jack and Vollmer, Michael and Batty, Mark},
title = {{Spegion: Implicit and Non-Lexical Regions with Sized Allocations}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {15:1--15:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.15},
URN = {urn:nbn:de:0030-drops-233082},
doi = {10.4230/LIPIcs.ECOOP.2025.15},
annote = {Keywords: Regions, Type Systems, Effect Systems, Programming Languages, Memory}
}
Document
A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework
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. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{izawa_et_al:LIPIcs.ECOOP.2025.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}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {16:1--16:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.16},
URN = {urn:nbn:de:0030-drops-233090},
doi = {10.4230/LIPIcs.ECOOP.2025.16},
annote = {Keywords: virtual machine, JIT compiler, multi-tier JIT compiler, meta-tracing JIT compiler, RPython}
}
Document
Contrasting Deadlock-Free Session Processes
Abstract
Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke et al.’s HCP, a type system based on a linear logic with hypersequents, and Padovani’s priority-based type system for asynchronous processes, dubbed 𝖯. Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by HCP and 𝖯. We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency.
Cite as
Juan C. Jaramillo and Jorge A. Pérez. Contrasting Deadlock-Free Session Processes. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jaramillo_et_al:LIPIcs.ECOOP.2025.17,
author = {Jaramillo, Juan C. and P\'{e}rez, Jorge A.},
title = {{Contrasting Deadlock-Free Session Processes}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {17:1--17:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.17},
URN = {urn:nbn:de:0030-drops-233103},
doi = {10.4230/LIPIcs.ECOOP.2025.17},
annote = {Keywords: session types, process calculi, deadlock freedom}
}
Document
Practical Type-Based Taint Checking and Inference
Abstract
Many important security properties can be formulated in terms of flows of tainted data, and improved taint analysis tools to prevent such flows are of critical need. Most existing taint analyses use whole-program static analysis, leading to scalability challenges. Type-based checking is a promising alternative, as it enables modular and incremental checking for fast performance. However, type-based approaches have not been widely adopted in practice, due to challenges with false positives and annotating existing codebases. In this paper, we present a new approach to type-based checking of taint properties that addresses these challenges, based on two key techniques. First, we present a new type-based tainting checker with significantly reduced false positives, via more practical handling of third-party libraries and other language constructs. Second, we present a novel technique to automatically infer tainting type qualifiers for existing code. Our technique supports inference of generic type argument annotations, crucial for tainting properties. We implemented our techniques in a tool TaintTyper and evaluated it on real-world benchmarks. TaintTyper exceeds the recall of a state-of-the-art whole-program taint analyzer, with comparable precision, and 2.93X-22.9X faster checking time. Further, TaintTyper infers annotations comparable to those written by hand, suitable for insertion into source code. TaintTyper is a promising new approach to efficient and practical taint checking.
Cite as
Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi. Practical Type-Based Taint Checking and Inference. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 18:1-18:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{karimipour_et_al:LIPIcs.ECOOP.2025.18,
author = {Karimipour, Nima and Das, Kanak and Sridharan, Manu and Hassanshahi, Behnaz},
title = {{Practical Type-Based Taint Checking and Inference}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {18:1--18:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.18},
URN = {urn:nbn:de:0030-drops-233119},
doi = {10.4230/LIPIcs.ECOOP.2025.18},
annote = {Keywords: Static analysis, Taint Analysis, Pluggable type systems, Security, Inference}
}
Document
Profile-Guided Field Externalization in an Ahead-Of-Time Compiler
Abstract
Field externalization is a technique to reduce the footprint of objects by removing fields that most frequently contain zero or null. While researchers have developed ways to bring this optimization into the Java world, these have been limited to research compilers or virtual machines for embedded systems. In this work, we present a novel field externalization technique that uses information from static analysis and profiling to determine externalizable fields. During compilation, we remove those fields and define companion classes. These are used in case of non-default-value writes to the externalized fields. Our approach also correctly handles synchronization to prevent issues in multithreaded environments. We integrated our approach into the modern Java ahead-of-time compiler GraalVM Native Image. We conducted an evaluation on a diverse set of benchmarks that includes standard and microservice-based benchmarks. For standard benchmarks, our approach reduces the total allocated bytes by 2.76% and the maximum resident set size (max-RSS) by 2.55%. For microservice benchmarks, we achieved a reduction of 6.88% for normalized allocated bytes and 2.45% for max-RSS. We computed these improvements via the geometric mean. The median reductions are are 1.46% (alloc. bytes) and 0.22% (max-RSS) in standard benchmarks, as well as 3.63% (alloc. bytes) and 0.20% (max-RSS) in microservice benchmarks.
Cite as
Sebastian Kloibhofer, Lukas Makor, Peter Hofer, David Leopoldseder, and Hanspeter Mössenböck. Profile-Guided Field Externalization in an Ahead-Of-Time Compiler. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 19:1-19:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kloibhofer_et_al:LIPIcs.ECOOP.2025.19,
author = {Kloibhofer, Sebastian and Makor, Lukas and Hofer, Peter and Leopoldseder, David and M\"{o}ssenb\"{o}ck, Hanspeter},
title = {{Profile-Guided Field Externalization in an Ahead-Of-Time Compiler}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {19:1--19:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.19},
URN = {urn:nbn:de:0030-drops-233121},
doi = {10.4230/LIPIcs.ECOOP.2025.19},
annote = {Keywords: compilation, instrumentation, profiling, fields, externalization, memory footprint reduction, memory footprint optimization}
}
Document
Incremental Computing by Differential Execution
Abstract
Incremental computing offers the potential for significant performance gains by efficiently updating computations in response to changing data. However, traditional approaches are either problem-specific or use an inefficient all-or-nothing strategy of rerunning affected computations entirely. This paper presents differential semantics, a novel approach that directly embeds the propagation of changes into the semantics of a general-purpose programming language. Given a precise description of input changes, differential semantics rules define how these changes are tracked and propagated through core language constructs like assignments, conditionals, and loops to produce corresponding output changes. We formalize differential semantics and verify key properties, including correctness, using the Rocq proof assistant. We also develop and formally prove a set of optimizations, particularly for loop handling, that enable asymptotic performance improvements. An implementation of the semantics as a differential interpreter achieves order-of-magnitude speedups over recomputation on the Bellman-Ford shortest path algorithm.
Cite as
Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kumar_et_al:LIPIcs.ECOOP.2025.20,
author = {Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
title = {{Incremental Computing by Differential Execution}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {20:1--20:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.20},
URN = {urn:nbn:de:0030-drops-233137},
doi = {10.4230/LIPIcs.ECOOP.2025.20},
annote = {Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics}
}
Document
GSOHC: Global Synchronization Optimization in Heterogeneous Computing
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 speedups of up to 1.8x, 1.9x and 1.9x over the baseline, respectively.
Cite as
Soumik Kumar Basu and Jyothi Vedurada. GSOHC: Global Synchronization Optimization in Heterogeneous Computing. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 21:1-21:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kumarbasu_et_al:LIPIcs.ECOOP.2025.21,
author = {Kumar Basu, Soumik and Vedurada, Jyothi},
title = {{GSOHC: Global Synchronization Optimization in Heterogeneous Computing}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {21:1--21:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.21},
URN = {urn:nbn:de:0030-drops-232949},
doi = {10.4230/LIPIcs.ECOOP.2025.21},
annote = {Keywords: Static Analysis, Synchronization, CPU-GPU, Heterogeneous Computing, Parallelization}
}
Document
Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions
Abstract
We propose an improved abstract interpretation based method for quantifying cache side-channel leakage by addressing two key components of precision loss in existing set-based cache abstractions. Our method targets two key sources of imprecision: (1) imprecision in the abstract transfer function used to update the abstract cache state when interpreting a memory access and (2) imprecision due to the incompleteness of the set-based domain. At the center of our method are two key improvements: (1) the introduction of a new transfer function for updating the abstract cache state which carefully leverages information in the abstract state to prevent the spurious aging of memory blocks and (2) a refinement of the set-based domain based on the finite powerset construction. We show that both the new abstract transformer and the domain refinement enjoy certain enhanced precision properties. We have implemented the method and compared it against the state-of-the-art technique on a suite of benchmark programs implementing both sorting algorithms and cryptographic algorithms. The experimental results show that our method is effective in improving the precision of cache side-channel leakage quantification.
Cite as
Jacqueline L. Mitchell and Chao Wang. Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mitchell_et_al:LIPIcs.ECOOP.2025.22,
author = {Mitchell, Jacqueline L. and Wang, Chao},
title = {{Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {22:1--22:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.22},
URN = {urn:nbn:de:0030-drops-233140},
doi = {10.4230/LIPIcs.ECOOP.2025.22},
annote = {Keywords: Abstract interpretation, side-channel, leakage quantification, cache}
}
Document
Wastrumentation: Portable WebAssembly Dynamic Analysis with Support for Intercession
Abstract
Dynamic program analyses help in understanding a program’s runtime behavior and detect issues related to security, program comprehension, or profiling. Instrumentation platforms aid analysis developers by offering a high-level API to write the analysis, and inserting the analysis into the target program. However, current instrumentation platforms for WebAssembly (Wasm) restrict analysis portability because they require concrete runtime environments. Moreover, their analysis API only allows the development of analyses that observe the target program but cannot modify it. As a result, many popular dynamic analyses present for other languages, such as runtime hardening, virtual patching or runtime optimization, cannot currently be implemented for Wasm atop a dynamic analysis platform. Instead, they need to be built manually, which requires knowledge of low-level details of the Wasm’s semantics and instruction set, and how to safely manipulate it.
This paper introduces Wastrumentation, the first dynamic analysis platform for WebAssembly that supports intercession. Our solution, based on source code instrumentation, weaves the analysis code directly into the target program code. Inlining the analysis into the target’s source code avoids dependencies on the runtime environment, making analyses portable across Wasm VMs. Moreover, it enables the implementation of analyses in any Wasm-compatible language. We evaluate our solution in two ways. First, we compare it against a state-of-the-art source code instrumentation platform using the WasmR3 benchmarks. The results show improved memory consumption and competitive performance overhead. Second, we develop an extensive portfolio of dynamic analyses, including novel analyses previously unattainable with source code instrumentation platforms, such as memoization, safe heap access, and the removal of NaN non-determinism.
Cite as
Aäron Munsters, Angel Luis Scull Pupo, and Elisa Gonzalez Boix. Wastrumentation: Portable WebAssembly Dynamic Analysis with Support for Intercession. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 23:1-23:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{munsters_et_al:LIPIcs.ECOOP.2025.23,
author = {Munsters, A\"{a}ron and Scull Pupo, Angel Luis and Gonzalez Boix, Elisa},
title = {{Wastrumentation: Portable WebAssembly Dynamic Analysis with Support for Intercession}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {23:1--23:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.23},
URN = {urn:nbn:de:0030-drops-233153},
doi = {10.4230/LIPIcs.ECOOP.2025.23},
annote = {Keywords: WebAssembly, dynamic analysis, instrumentation platform, intercession}
}
Document
Fair Termination of Asynchronous Binary Sessions
Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as
Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
author = {Padovani, Luca and Zavattaro, Gianluigi},
title = {{Fair Termination of Asynchronous Binary Sessions}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {24:1--24:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.24},
URN = {urn:nbn:de:0030-drops-233169},
doi = {10.4230/LIPIcs.ECOOP.2025.24},
annote = {Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
Reusing Highly Optimized IR in Dynamic Compilation
Abstract
Virtual machines (VMs) with dynamic compilers typically specialize compiled code to the state of the running VM instance and thus cannot reuse the code between multiple runs of the same application. The JIT compiler must recompile the same methods for each run of the application separately, which can prolong the application’s warmup time. We propose a technique to reduce compilation time by reusing a highly optimized intermediate representation (IR). We achieve this by tracing compiler-interface calls during compilation. The validity of the specializations in the IR is verified during a replay stage, and the replay also facilitates the relocation of runtime object references. The IR is stored on a compilation server, which can compile it to machine code and provide the code to local or remote VM instances. We implemented a compilation server with IR caching for GraalVM, a high-performance production-grade Java Virtual Machine (JVM). We present an evaluation based on four industry-standard benchmark suites. In each suite, our approach reduces compilation time by 23.6% to 36.8% and warmup time by 13.1% to 21.2% on average while preserving peak application performance.
Cite as
Andrej Pečimúth, David Leopoldseder, and Petr Tůma. Reusing Highly Optimized IR in Dynamic Compilation. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 25:1-25:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{pecimuth_et_al:LIPIcs.ECOOP.2025.25,
author = {Pe\v{c}im\'{u}th, Andrej and Leopoldseder, David and T\r{u}ma, Petr},
title = {{Reusing Highly Optimized IR in Dynamic Compilation}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {25:1--25:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.25},
URN = {urn:nbn:de:0030-drops-233176},
doi = {10.4230/LIPIcs.ECOOP.2025.25},
annote = {Keywords: code reuse, compilation time, warmup, remote compilation, dynamic compilation, virtual machines}
}
Document
Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design
Abstract
Tools such as Alloy enable users to incrementally define, explore, verify, and diagnose specifications for complex systems. A critical component of these tools is a visualizer that lets users graphically explore generated models. As we show, however, a default visualizer that knows nothing about the domain can be unhelpful and can even actively violate presentational and cognitive principles. At the other extreme, full-blown custom visualization requires significant effort as well as knowledge that a tool user might not possess. Custom visualizations can also exhibit bad (even silent) failures.
This paper charts a middle ground between the extremes of default and fully-customizable visualization. We capture essential domain information for lightweight diagramming, embodying this in a language. To identify key elements of lightweight diagrams, we ground the language design in both the cognitive science research on diagrams and in a corpus of 58 custom visualizations. We distill from these sources a small set of orthogonal primitives, and use the primitives to guide a diagramming language called Cope-and-Drag (CnD). We evaluate it on sample tasks, three user studies, and performance, and find that short CnD specifications consistently improve model comprehension over the Alloy default. CnD thus defines a new point in the design space of diagramming: a language that is lightweight, effective, and driven by sound principles.
Cite as
Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 26:1-26:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{prasad_et_al:LIPIcs.ECOOP.2025.26,
author = {Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
title = {{Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {26:1--26:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.26},
URN = {urn:nbn:de:0030-drops-233187},
doi = {10.4230/LIPIcs.ECOOP.2025.26},
annote = {Keywords: formal methods, diagramming, visualization, language design}
}
Document
PoTo: A Hybrid Andersen’s Points-To Analysis for Python
Abstract
As Python is increasingly being adopted for large and complex programs, the importance of static analysis for Python (such as type inference) grows. Unfortunately, static analysis for Python remains a challenging task due to its dynamic language features and its abundant external libraries. To help fill this gap, this paper presents PoTo, an Andersen-style context-insensitive and flow-insensitive points-to analysis for Python. PoTo addresses Python-specific challenges and works for large programs via a novel hybrid evaluation, integrating traditional static points-to analysis with concrete evaluation in the Python interpreter for external library calls. We evaluate the analysis with two clients: type inference and call graph construction. This paper presents PoTo+, a static type inference for Python built on PoTo. We evaluate PoTo+ and compare it to two state-of-the-art Python type inference techniques: (1) the static rule-based Pytype and (2) the deep-learning based DLInfer. Our results show that PoTo+ outperforms both Pytype and DLInfer on existing Python packages. This paper also presents PoToCG, a call-graph construction analysis for Python built on PoTo. We compare PoToCG to PyCG, the state of the art for this problem, and show that PoTo produces more complete and more precise call graphs.
Cite as
Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, and Julian Dolby. PoTo: A Hybrid Andersen’s Points-To Analysis for Python. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 27:1-27:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{rakamnouykit_et_al:LIPIcs.ECOOP.2025.27,
author = {Rak-amnouykit, Ingkarat and Milanova, Ana and Baudart, Guillaume and Hirzel, Martin and Dolby, Julian},
title = {{PoTo: A Hybrid Andersen’s Points-To Analysis for Python}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {27:1--27:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.27},
URN = {urn:nbn:de:0030-drops-233194},
doi = {10.4230/LIPIcs.ECOOP.2025.27},
annote = {Keywords: Python, Points-to analysis, Machine learning libraries}
}
Document
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis
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 C 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, Antoine Miné, Valentin Perrelle, and Julien Signoles. Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{razafintsialonina_et_al:LIPIcs.ECOOP.2025.28,
author = {Razafintsialonina, Mamy and B\"{u}hler, David and Min\'{e}, Antoine and Perrelle, Valentin and Signoles, Julien},
title = {{Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {28:1--28:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.28},
URN = {urn:nbn:de:0030-drops-233207},
doi = {10.4230/LIPIcs.ECOOP.2025.28},
annote = {Keywords: Abstract Interpretation, Static Analysis, Incremental Analysis}
}
Document
Declarative Dynamic Object Reclassification
Abstract
In object-oriented languages, dynamic object reclassification is a technique to change the class binding of an object at runtime. Current approaches express when and how to reclassify inside the program’s business code, while maintaining internal consistency. These approaches are less suited for programs that need to be consistent with an external context, such as autonomous systems interacting with a knowledge base. This paper proposes declarative dynamic object reclassification, a novel technique that provides a separation of concerns between a program’s business code and its adaptation logic for reclassification, expressed via a knowledge base. We present Featherweight Semantically Reflected Java, a minimal calculus for declarative dynamic object reclassification that enables the programmer to define consistency both internally (using a type system) and externally (using declarative classification queries). We use this calculus to study how internal and external consistency interact for declarative dynamic object reclassification. We further implement the technique by extending SMOL, a language for reflective programming via external knowledge bases.
Cite as
Riccardo Sieve, Eduard Kamburjan, Ferruccio Damiani, and Einar Broch Johnsen. Declarative Dynamic Object Reclassification. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 29:1-29:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sieve_et_al:LIPIcs.ECOOP.2025.29,
author = {Sieve, Riccardo and Kamburjan, Eduard and Damiani, Ferruccio and Johnsen, Einar Broch},
title = {{Declarative Dynamic Object Reclassification}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {29:1--29:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.29},
URN = {urn:nbn:de:0030-drops-233211},
doi = {10.4230/LIPIcs.ECOOP.2025.29},
annote = {Keywords: Dynamic Object Reclassification, Dynamic Software Updates, Featherweight Java, Knowledge Bases, Semantic Reflection, Type Soundness}
}
Document
In-Memory Object Graph Stores
Abstract
We present a design and implementation of an in-memory object graph store, dubbed εStore. Our key innovation is a storage model - epsilon store - that equates an object on the heap to a node in a graph store. Thus any object on the heap (without changes) can be a part of one, or multiple, graph stores, and vice versa, any node in a graph store can be accessed like any other object on the heap. Specifically, each node in a graph is an object (i.e., instance of a class), and its properties and its edges are the primitive and reference fields declared in its class, respectively. Necessary classes, which are instantiated to represent nodes, are created dynamically by εStore. εStore uses a subset of the Cypher query language to query the graph store. By design, the result of any query is a table (ResultSet) of references to objects on the heap, which users can manipulate the same way as any other object on the heap in their programs. Moreover, a developer can include (transitively) an arbitrary object to become a part of a graph store. Finally, εStore introduces compile-time rewriting of Cypher queries into imperative code to improve the runtime performance. εStore can be used for a number of tasks including implementing methods for complex in-memory structures, writing complex assertions, or a stripped down version of a graph database that can conveniently be used during testing. We implement εStore in Java and show its application using the aforementioned tasks.
Cite as
Aditya Thimmaiah, Zijian Yi, Joseph Kenis, Christopher J Rossbach, and Milos Gligoric. In-Memory Object Graph Stores. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 30:1-30:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{thimmaiah_et_al:LIPIcs.ECOOP.2025.30,
author = {Thimmaiah, Aditya and Yi, Zijian and Kenis, Joseph and Rossbach, Christopher J and Gligoric, Milos},
title = {{In-Memory Object Graph Stores}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {30:1--30:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.30},
URN = {urn:nbn:de:0030-drops-233225},
doi = {10.4230/LIPIcs.ECOOP.2025.30},
annote = {Keywords: Object stores, Graph stores, Cypher}
}
Document
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction
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.
Cite as
Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 31:1-31:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{tirore_et_al:LIPIcs.ECOOP.2025.31,
author = {Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
title = {{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {31:1--31:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.31},
URN = {urn:nbn:de:0030-drops-233238},
doi = {10.4230/LIPIcs.ECOOP.2025.31},
annote = {Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
Compositional Static Value Analysis for Higher-Order Numerical Programs
Abstract
Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their recursive functions, recursive algebraic data types, and higher-order functions. Classic type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants.
Our work describes a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. The summaries can be viewed as input-output relations expressed with relational abstract domains. We present two new abstract domains. A first abstract domain summarizes recursive algebraic data types. A second abstract domain lifts existing disjunctive relational summaries to higher-order by formalizing them as domains able to abstract higher-order functions. Both abstractions are parameterized by the abstractions of basic types (strings, integers, ...). Thanks to this parametric nature, both domains can be combined, allowing the analysis of higher-order functions manipulating algebraic data types and, conversely, algebraic data types using functions as first-class values.
We have implemented this analysis in the open-source MOPSA platform. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs as well as 20 programs from the state-of-the-art Salto analyzer benchmark.
Cite as
Milla Valnet, Raphaël Monat, and Antoine Miné. Compositional Static Value Analysis for Higher-Order Numerical Programs. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 32:1-32:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{valnet_et_al:LIPIcs.ECOOP.2025.32,
author = {Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
title = {{Compositional Static Value Analysis for Higher-Order Numerical Programs}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {32:1--32:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.32},
URN = {urn:nbn:de:0030-drops-233249},
doi = {10.4230/LIPIcs.ECOOP.2025.32},
annote = {Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
Mono Types - First-Class Containers for Datalog
Abstract
We propose mono types, a new abstraction for programming Datalog. Mono types behave like first-class containers that can be stored in relations and to which elements can be added decentrally. But, mono types are more than just containers: They provide a read operation that can yield any result as long as it monotonically grows with each added element and is independent of the order in which elements are added to the container. This design permits a wide range of mono types (e.g., sets, maps, and aggregations), yet guarantees mono types can be integrated into Datalog without jeopardizing Datalog’s least fixed-point semantics. We develop a theory for mono types, which includes constructions for complex mono types, equivalence relation for mono types, and properties about semantics-preserving mono-type transformations. This theory ensures sound Datalog integration and justifies crucial compiler optimizations for mono types. Together, these techniques demonstrate that mono types provide abstraction without regret: We demonstrate in two case studies that programs become easier to write with mono types, while their performance also improves drastically.
Cite as
Runqing Xu, David Klopp, and Sebastian Erdweg. Mono Types - First-Class Containers for Datalog. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 33:1-33:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{xu_et_al:LIPIcs.ECOOP.2025.33,
author = {Xu, Runqing and Klopp, David and Erdweg, Sebastian},
title = {{Mono Types - First-Class Containers for Datalog}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {33:1--33:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.33},
URN = {urn:nbn:de:0030-drops-233250},
doi = {10.4230/LIPIcs.ECOOP.2025.33},
annote = {Keywords: Datalog, compiler optimization}
}
Document
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering
Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection.
To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs.
We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as
Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
author = {Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
title = {{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {34:1--34:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.34},
URN = {urn:nbn:de:0030-drops-233265},
doi = {10.4230/LIPIcs.ECOOP.2025.34},
annote = {Keywords: Abstract interpretation, recursion, weak topological ordering}
}
Document
Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation
Abstract
The use of Large Language Models (LLMs) for code generation has gained significant attention in recent years. Existing methods often aim to improve the quality of generated code by incorporating additional contextual information or guidance into input prompts. Many of these approaches adopt process-oriented reasoning strategies, mimicking human-like step-by-step thinking; however, they may not always align with the structured nature of programming languages. This paper introduces Chain of Grounded Objectives (CGO), a concise goal-oriented prompting approach that embeds functional objectives into prompts to enhance code generation. By focusing on precisely defined objectives rather than explicit procedural steps, CGO aligns more naturally with programming tasks while retaining flexibility. Empirical evaluations on HumanEval, MBPP, their extended versions, and LiveCodeBench show that CGO achieves accuracy comparable to or better than existing methods while using fewer tokens, making it a more efficient approach to LLM-based code generation.
Cite as
Sangyeop Yeo, Seung-Won Hwang, and Yu-Seung Ma. Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{yeo_et_al:LIPIcs.ECOOP.2025.35,
author = {Yeo, Sangyeop and Hwang, Seung-Won and Ma, Yu-Seung},
title = {{Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {35:1--35:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.35},
URN = {urn:nbn:de:0030-drops-233271},
doi = {10.4230/LIPIcs.ECOOP.2025.35},
annote = {Keywords: Artificial Intelligence, Natural Language Processing, Prompt Design, Large Language Models, Code Generation}
}
Document
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
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 are necessary 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 to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with 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, in order 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-problems 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. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 36:1-36:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zhang_et_al:LIPIcs.ECOOP.2025.36,
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}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {36:1--36:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.36},
URN = {urn:nbn:de:0030-drops-233281},
doi = {10.4230/LIPIcs.ECOOP.2025.36},
annote = {Keywords: neural network verification, branch and bound, counterexample potentiality, simulated annealing, stochastic optimization}
}
Document
Experience Paper
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)
Abstract
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
Cite as
Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dacik_et_al:LIPIcs.ECOOP.2025.37,
author = {Dac{\'\i}k, Tom\'{a}\v{s} and Vojnar, Tom\'{a}\v{s}},
title = {{RacerF: Lightweight Static Data Race Detection for C Code}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {37:1--37:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.37},
URN = {urn:nbn:de:0030-drops-233298},
doi = {10.4230/LIPIcs.ECOOP.2025.37},
annote = {Keywords: concurrency, data race detection, static analysis}
}
Document
Experience Paper
Type-Safe and Portable Support for Packed Data (Experience Paper)
Abstract
When components of a system exchange data, they need to serialise the data so that it can be sent over the network. Then, the recipient has to deserialise the data in order to be able to process it. These steps take time and have an impact on the overall system’s performance.
A solution to this is to use packed data, which has a unified representation between the memory and the network, removing the need for any marshalling steps. Additionally, using this data representation can improve the program’s performance thanks to the data locality enabled by the compact representation of the data in memory. Unfortunately, no mainstream programming languages support packed data, whether it’s out-of-the-box or through a compiler extension.
We present packed-data, a Haskell library that allows for type safe building and reading of packed data in a functional style. The library does not rely on compiler modifications, making it portable, and leverages meta-programming to allow programmers to pack their own data types effortlessly.
We evaluate the usability and performance of the library, and conclude that it allows traversing packed data up to 60% faster than unpacked data. We also reflect on how to enhance the performance of library-based support for packed data.
Our implementation approach is general and can easily be used with any programming languages that support higher-kinded types.
Cite as
Arthur Jamet and Michael Vollmer. Type-Safe and Portable Support for Packed Data (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jamet_et_al:LIPIcs.ECOOP.2025.38,
author = {Jamet, Arthur and Vollmer, Michael},
title = {{Type-Safe and Portable Support for Packed Data}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {38:1--38:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.38},
URN = {urn:nbn:de:0030-drops-233301},
doi = {10.4230/LIPIcs.ECOOP.2025.38},
annote = {Keywords: program optimisation, data structures, data layout, packed data}
}
Document
Experience Paper
WebGlitch: A Randomised Testing Tool for the WebGPU API (Experience Paper)
Abstract
We report on our experience designing a new technique and tool for fuzzing implementations of WebGPU, a W3C standard JavaScript API for in-browser GPU computing. We also report on our experience using our WebGlitch tool to test industrial-strength implementations of WebGPU, leading to the discovery of numerous bugs. WebGPU enables programmatic access to a device’s graphics processing unit (GPU) for in-browser GPU computing, and is being implemented by Google, Mozilla and Apple for inclusion in all of the major web browsers. Guaranteeing the security and reliability of WebGPU is crucial to avoid wide-reaching browser security vulnerabilities and to facilitate portability by ensuring uniform behaviour across different platforms. To that end - inspired by randomised compiler testing techniques - our approach to fuzzing creates random, valid-by-construction programs by continuously selecting a WebGPU API function, then recursively generating all requirements necessary for that API call to be valid based on careful modelling of the API specification. This is implemented as a new open source tool, WebGlitch, which we designed in consultation with engineers at Google who work on the Chrome WebGPU implementation. WebGlitch identifies bugs through sanitiser-boosted crash oracles, differential testing, and by identifying cases where valid-by-construction API calls lead to runtime errors. We present an evaluation showing that WebGlitch can find bugs missed by an existing WebGPU fuzzer, wg-fuzz, and across the broader WebGPU ecosystem: to date, WebGlitch has found 24 previously-unknown bugs (15 fixed so far in response to our reports). Among these, 17 bugs affected WebGPU implementations from Google, Mozilla, and the Deno project. WebGlitch found an additional 4 bugs in the shader compilers used by the graphics APIs that WebGPU interfaces with. The remaining 3 bugs affect the widely-used JavaScript runtimes Node.js and Deno. Fuzzing with WebGlitch also led us to identify an ambiguity in the specification of the WebGPU shading language, for which we proposed an amendment that was accepted by W3C and which has been adopted in the latest version of the specification. Analysing the line coverage of a WebGPU implementation by WebGlitch-generated programs revealed that WebGlitch covers code missed by wg-fuzz and the official conformance test suite. Our hope is that this report on the design of WebGlitch and its deployment in practice will be useful for practitioners and researchers interested in using API fuzzing to improve the reliability of industrial codebases.
Cite as
Matthew K. L. Wong and Alastair F. Donaldson. WebGlitch: A Randomised Testing Tool for the WebGPU API (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 39:1-39:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{wong_et_al:LIPIcs.ECOOP.2025.39,
author = {Wong, Matthew K. L. and Donaldson, Alastair F.},
title = {{WebGlitch: A Randomised Testing Tool for the WebGPU API}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {39:1--39:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.39},
URN = {urn:nbn:de:0030-drops-233313},
doi = {10.4230/LIPIcs.ECOOP.2025.39},
annote = {Keywords: Fuzzing, WebGPU, WGSL, API, shaders}
}
Document
Replication Paper
Scaling Up: Revisiting Mining Android Sandboxes at Scale for Malware Classification (Replication Paper)
Abstract
The widespread use of smartphones in daily life has raised concerns about privacy and security among researchers and practitioners. Privacy issues are generally highly prevalent in mobile applications, particularly targeting the Android platform - the most popular mobile operating system. For this reason, several techniques have been proposed to identify malicious behavior in Android applications, including the Mining Android Sandbox approach (MAS approach), which aims to identify malicious behavior in repackaged Android applications (apps). However, previous empirical studies evaluated the MAS approach using a small dataset consisting of only 102 pairs of original and repackaged apps. This limitation raises questions about the external validity of their findings and whether the MAS approach can be generalized to larger datasets. To address these concerns, this paper presents the results of a replication study focused on evaluating the performance of the MAS approach regarding its capabilities of correctly classifying malware from different families. Unlike previous studies, our research employs a dataset that is an order of magnitude larger, comprising 4,076 pairs of apps covering a more diverse range of Android malware families. Surprisingly, our findings indicate a poor performance of the MAS approach for identifying malware, with the F1-score decreasing from 0.90 for the small dataset used in the previous studies to 0.54 in our more extensive dataset. Upon closer examination, we discovered that certain malware families partially account for the low accuracy of the MAS approach, which fails to classify a repackaged version of an app as malware correctly. Our findings highlight the limitations of the MAS approach, particularly when scaled, and underscore the importance of complementing it with other techniques to detect a broader range of malware effectively. This opens avenues for further discussion on addressing the blind spots that affect the accuracy of the MAS approach.
Cite as
Francisco Handrick Tomaz da Costa, Ismael Medeiros, Leandro Oliveira, João Calássio, Rodrigo Bonifácio, Krishna Narasimhan, Mira Mezini, and Márcio Ribeiro. Scaling Up: Revisiting Mining Android Sandboxes at Scale for Malware Classification (Replication Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 40:1-40:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{handricktomazdacosta_et_al:LIPIcs.ECOOP.2025.40,
author = {Handrick Tomaz da Costa, Francisco and Medeiros, Ismael and Oliveira, Leandro and Cal\'{a}ssio, Jo\~{a}o and Bonif\'{a}cio, Rodrigo and Narasimhan, Krishna and Mezini, Mira and Ribeiro, M\'{a}rcio},
title = {{Scaling Up: Revisiting Mining Android Sandboxes at Scale for Malware Classification}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {40:1--40:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.40},
URN = {urn:nbn:de:0030-drops-233320},
doi = {10.4230/LIPIcs.ECOOP.2025.40},
annote = {Keywords: Android Malware Detection, Dynamic Analysis, Mining Android Sandboxes}
}
Document
Pearl/Brave New Idea
Shouting at Memory: Where Did My Write Go? (Pearl/Brave New Idea)
Abstract
Non-Volatile Memory (NVM) promises persistent data, but verifying that promise on real hardware is challenging due to opaque caching and internal buffers like Intel’s WPQ, which obscure the true state of writes. Traditional validation methods often fall short. This paper introduces a novel perspective: leveraging the subtle timing variations of memory accesses as a direct probe into write persistence.
We present a software technique, inspired by echolocation, that uses high-resolution timers to measure memory load latencies. These timings act as distinct signatures ("echoes") revealing whether a write’s data resides in volatile caches or has reached the NVM persistence domain. This offers a non-invasive method to track write progression towards durability.
To reliably interpret these potentially noisy timing signatures and systematically explore complex persistence behaviours, we integrate this echolocation probe into an active model learning framework. This synergy enables the automated inference of a system’s actual persistency semantics directly from black-box hardware observations. The approach is hardware-agnostic, adaptive, and scalable. Preliminary experiments on Intel x86 - a platform where persistence validation is notably challenged by the opaque Write Pending Queue (WPQ) - demonstrate the feasibility of our technique. We observed distinct latency clusters differentiating volatile cache accesses from those reaching the persistence domain. This combined approach offers a promising path towards robust and automated validation of NVM persistency across diverse architectures.
Cite as
Vasileios Klimis. Shouting at Memory: Where Did My Write Go? (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 41:1-41:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{klimis:LIPIcs.ECOOP.2025.41,
author = {Klimis, Vasileios},
title = {{Shouting at Memory: Where Did My Write Go?}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {41:1--41:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.41},
URN = {urn:nbn:de:0030-drops-233339},
doi = {10.4230/LIPIcs.ECOOP.2025.41},
annote = {Keywords: Persistency Memory Semantics, Fuzz Testing, Model Learning}
}
Document
Pearl/Brave New Idea
Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)
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, this paper 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 (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{moy_et_al:LIPIcs.ECOOP.2025.42,
author = {Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
title = {{Contract Systems Need Domain-Specific Notations}},
booktitle = {39th European Conference on Object-Oriented Programming (ECOOP 2025)},
pages = {42:1--42:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-373-7},
ISSN = {1868-8969},
year = {2025},
volume = {333},
editor = {Aldrich, Jonathan 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.2025.42},
URN = {urn:nbn:de:0030-drops-233348},
doi = {10.4230/LIPIcs.ECOOP.2025.42},
annote = {Keywords: software contracts, domain-specific languages}
}