21 Search Results for "Muller, Gilles"

Document
DOI: 10.4230/OASIcs.NINeS.2026.13
In-Kernel Aggregation and Broadcast Acceleration for Distributed Communication

Authors: Jianchang Su, Yifan Zhang, and Wei Zhang

Published in: OASIcs, Volume 139, 1st New Ideas in Networked Systems (NINeS 2026)

Abstract
Broadcasting and aggregation dominate the communication overhead in distributed systems, from machine learning training to data analytics. Current acceleration approaches require specialized hardware (RDMA) or dedicated resources (DPDK), limiting their deployment in commodity clouds. However, we present a counter-intuitive alternative: rather than bypassing the kernel, we move operations into it using eBPF. While this imposes severe constraints including no floating-point, limited memory, and stateless execution, we show these restrictions paradoxically drive innovative protocol designs that yield unexpected benefits. We introduce AggBox, which implements broadcast and aggregation operations entirely within eBPF’s constrained environment. Our key innovations include stateless group acknowledgments for reliability, edge quantization for floating-point aggregation using only integer arithmetic, and tail-call chains that create virtual memory beyond eBPF’s 512-byte stack limit. These designs emerge from and exploit the constraints rather than fighting them. AggBox achieves remarkable performance on commodity hardware: 84.5% reduction in broadcast latency, 43× speedup for MapReduce workloads, and 56.1% faster ML gradient aggregation, all without specialized NICs or dedicated cores. Beyond performance, our work demonstrates that constrained environments can drive fundamental innovation in protocol design, offering insights for future resource-limited and verified systems.
Cite as

Jianchang Su, Yifan Zhang, and Wei Zhang. In-Kernel Aggregation and Broadcast Acceleration for Distributed Communication. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{su_et_al:OASIcs.NINeS.2026.13,
  author =	{Su, Jianchang and Zhang, Yifan and Zhang, Wei},
  title =	{{In-Kernel Aggregation and Broadcast Acceleration for Distributed Communication}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{13:1--13:23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-414-7},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{139},
  editor =	{Argyraki, Katerina and Panda, Aurojit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NINeS.2026.13},
  URN =		{urn:nbn:de:0030-drops-255981},
  doi =		{10.4230/OASIcs.NINeS.2026.13},
  annote =	{Keywords: eBPF, distributed communication, broadcast, aggregation, in-kernel processing, XDP}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.5
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Authors: Joshua M. Cohen

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.
Cite as

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.ITP.2025.5,
  author =	{Cohen, Joshua M.},
  title =	{{A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.5},
  URN =		{urn:nbn:de:0030-drops-246046},
  doi =		{10.4230/LIPIcs.ITP.2025.5},
  annote =	{Keywords: Pattern Matching Compilation, Algebraic Data Types, First-Order Logic}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.26
Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks

Authors: David Andrew Green

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
The Artemis programme seeks to develop and test concepts, hardware and approaches to support long term habitation of the Lunar surface, and future missions to Mars. In preparation for the Artemis missions determination of tasks to be performed, the functional requirements of such tasks and as mission duration extends whether physiological deconditioning becomes functionally significant, compromising the crew member’s ability to perform critical tasks on the surface, and/or upon return to earth [MoLo-LUNA – leveraging the Molo programme (and several other activities) - could become a key supporting activity for LUNA incl. validation of the Puppeteer offloading system itself via creation of a complementary MoLo-LUNA-LAB. Furthermore, the MoLo-LUNA programme could become a key facilitator of simulator suit instrumentation/definition, broader astronaut training activities and mission architecture development – including Artemis mission simulations. By employing a Puppeteer system external to the LUNA chamber hall it will optimise utilisation and cost-effectiveness of LUNA, and as such represents a critical service to future LUNA stakeholders. Furthermore, MoLo-LUNA would generate a unique data set that can be leveraged to predict de-conditioning on the Lunar surface - and thereby optimise functionality, and minimise mission risk – including informing the need for, and prescription of exercise countermeasures on the Lunar Surface and in transit. Thus, MoLo-LUNA offers a unique opportunity to place LUNA, and ESA as a key ongoing provider of evidence to define, optimise and support crew Artemis surface missions.
Cite as

David Andrew Green. Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 26:1-26:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{green:OASIcs.SpaceCHI.2025.26,
  author =	{Green, David Andrew},
  title =	{{Movement in Low Gravity (MoLo) – LUNA: Biomechanical Modelling to Mitigate Lunar Surface Operation Risks}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{26:1--26:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.26},
  URN =		{urn:nbn:de:0030-drops-240166},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.26},
  annote =	{Keywords: Locomotion, hypogravity, modelling, Lunar}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.23
The Pyttern Program Query Language

Authors: Julien Liénard, Kim Mens, and Siegfried Nijssen

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
Despite the availability of numerous tools and languages for detecting structural patterns in programs, their complexity often presents a steep learning curve. This highlights the need for a program query language that is easier to learn, use, and read while remaining sufficiently expressive for defining and detecting relevant structural coding patterns in program code. To address this challenge, we present Pyttern, a query language that extends Python syntax with regular-expression-inspired wildcards, enabling intuitive pattern-based querying of Python code. Its implementation relies upon a custom pushdown automaton describing how to match patterns over program parse trees, thus providing a robust foundation for structural code analysis. We evaluate Pyttern’s usability and effectiveness through a study involving 35 master’s students, who were asked to write seven different patterns to identify known programming misconceptions. The results demonstrate that Pyttern is both easy to learn and practical to use, at least for analysing small-scale programs.
Cite as

Julien Liénard, Kim Mens, and Siegfried Nijssen. The Pyttern Program Query Language. In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lienard_et_al:OASIcs.Programming.2025.23,
  author =	{Li\'{e}nard, Julien and Mens, Kim and Nijssen, Siegfried},
  title =	{{The Pyttern Program Query Language}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{23:1--23:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.23},
  URN =		{urn:nbn:de:0030-drops-243075},
  doi =		{10.4230/OASIcs.Programming.2025.23},
  annote =	{Keywords: Pyttern, Program Query Languages, Python, Pattern Matching, Parse Tree, Pushdown Automaton, Static Code Analysis, Wildcards, Tree Pattern Matching}
}
Document
DOI: 10.4230/LIPIcs.DNA.31.4
Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems

Authors: Inhoo Lee, Salvador Buse, and Erik Winfree

Published in: LIPIcs, Volume 347, 31st International Conference on DNA Computing and Molecular Programming (DNA 31) (2025)

Abstract
Many molecular systems are best understood in terms of prototypical species and reactions. The central dogma and related biochemistry are rife with examples: gene i is transcribed into RNA i, which is translated into protein i; kinase n phosphorylates substrate m; protein p dimerizes with protein q. Engineered nucleic acid systems also often have this form: oligonucleotide i hybridizes to complementary oligonucleotide j; signal strand n displaces the output of seesaw gate m; hairpin p triggers the opening of target q. When there are many variants of a small number of prototypes, it can be conceptually cleaner and computationally more efficient to represent the full system in terms of indexed species (e.g. for dimerization, M_p, D_pq) and indexed reactions (M_p + M_q → D_pq). Here, we formalize the Indexed Chemical Reaction Network (ICRN) model and describe a Python software package designed to simulate such systems in the well-mixed and reaction-diffusion settings, using a differentiable programming framework originally developed for large-scale neural network models, taking advantage of GPU acceleration when available. Notably, this framework makes it straightforward to train the models’ initial conditions and rate constants to optimize a target behavior, such as matching experimental data, performing a computation, or exhibiting spatial pattern formation. The natural map of indexed chemical reaction networks onto neural network formalisms provides a tangible yet general perspective for translating concepts and techniques from the theory and practice of neural computation into the design of biomolecular systems.
Cite as

Inhoo Lee, Salvador Buse, and Erik Winfree. Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems. In 31st International Conference on DNA Computing and Molecular Programming (DNA 31). Leibniz International Proceedings in Informatics (LIPIcs), Volume 347, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.DNA.31.4,
  author =	{Lee, Inhoo and Buse, Salvador and Winfree, Erik},
  title =	{{Differentiable Programming of Indexed Chemical Reaction Networks and Reaction-Diffusion Systems}},
  booktitle =	{31st International Conference on DNA Computing and Molecular Programming (DNA 31)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-399-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{347},
  editor =	{Schaeffer, Josie and Zhang, Fei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.31.4},
  URN =		{urn:nbn:de:0030-drops-238534},
  doi =		{10.4230/LIPIcs.DNA.31.4},
  annote =	{Keywords: Differentiable Programming, Chemical Reaction Networks, Reaction-Diffusion Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
DOI: 10.4230/LIPIcs.CCC.2025.27
New Codes on High Dimensional Expanders

Authors: Irit Dinur, Siqi Liu, and Rachel Yun Zhang

Published in: LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025)

Abstract
We describe a new parameterized family of symmetric error-correcting codes with low-density parity-check matrices (LDPC). Our codes can be described in two seemingly different ways. First, in relation to Reed-Muller codes: our codes are functions on a subset of the points in 𝔽ⁿ whose restrictions to a prescribed set of affine lines has low degree. Alternatively, they are Tanner codes on high dimensional expanders, where the coordinates of the codeword correspond to triangles of a 2-dimensional expander, such that around every edge the local view forms a Reed-Solomon codeword. For some range of parameters our codes are provably locally testable, and their dimension is some fixed power of the block length. For another range of parameters our codes have distance and dimension that are both linear in the block length, but we do not know if they are locally testable. The codes also have the multiplication property: the coordinate-wise product of two codewords is a codeword in a related code. The definition of the codes relies on the construction of a specific family of simplicial complexes which is a slight variant on the coset complexes of Kaufman and Oppenheim. We show a novel way to embed the triangles of these complexes into 𝔽ⁿ, with the property that links of edges embed as affine lines in 𝔽ⁿ. We rely on this embedding to lower bound the rate of these codes in a way that avoids constraint-counting and thereby achieves non-trivial rate even when the local codes themselves have arbitrarily small rate, and in particular below 1/2.
Cite as

Irit Dinur, Siqi Liu, and Rachel Yun Zhang. New Codes on High Dimensional Expanders. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 27:1-27:42, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dinur_et_al:LIPIcs.CCC.2025.27,
  author =	{Dinur, Irit and Liu, Siqi and Zhang, Rachel Yun},
  title =	{{New Codes on High Dimensional Expanders}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{27:1--27:42},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-379-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{339},
  editor =	{Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.27},
  URN =		{urn:nbn:de:0030-drops-237217},
  doi =		{10.4230/LIPIcs.CCC.2025.27},
  annote =	{Keywords: error correcting codes, high dimensional expanders, multiplication property}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.21
An Expressive Trace Logic for Recursive Programs

Authors: Dilian Gurov and Reiner Hähnle

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Cite as

Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gurov_et_al:LIPIcs.FSCD.2025.21,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner},
  title =	{{An Expressive Trace Logic for Recursive Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.21},
  URN =		{urn:nbn:de:0030-drops-236360},
  doi =		{10.4230/LIPIcs.FSCD.2025.21},
  annote =	{Keywords: Denotational semantics, compositional semantics, program specification, compositional verification, fixed point logic, trace logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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
DOI: 10.4230/LIPIcs.ECOOP.2025.14
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

Authors: Matt Griffin, Brijesh Dongol, and Azalea Raad

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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
DOI: 10.4230/LIPIcs.ECOOP.2025.22
Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions

Authors: Jacqueline L. Mitchell and Chao Wang

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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
DOI: 10.4230/LIPIcs.ECOOP.2025.17
Contrasting Deadlock-Free Session Processes

Authors: Juan C. Jaramillo and Jorge A. Pérez

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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
Academic Track
DOI: 10.4230/OASIcs.SAIA.2024.12
A View on Vulnerabilites: The Security Challenges of XAI (Academic Track)

Authors: Elisabeth Pachl, Fabian Langer, Thora Markert, and Jeanette Miriam Lorenz

Published in: OASIcs, Volume 126, Symposium on Scaling AI Assessments (SAIA 2024)

Abstract
Modern deep learning methods have long been considered as black-boxes due to their opaque decision-making processes. Explainable Artificial Intelligence (XAI), however, has turned the tables: it provides insight into how these models work, promoting transparency that is crucial for accountability. Yet, recent developments in adversarial machine learning have highlighted vulnerabilities in XAI methods, raising concerns about security, reliability and trustworthiness, particularly in sensitive areas like healthcare and autonomous systems. Awareness of the potential risks associated with XAI is needed as its adoption increases, driven in part by the need to enhance compliance to regulations. This survey provides a holistic perspective on the security and safety landscape surrounding XAI, categorizing research on adversarial attacks against XAI and the misuse of explainability to enhance attacks on AI systems, such as evasion and privacy breaches. Our contribution includes identifying current insecurities in XAI and outlining future research directions in adversarial XAI. This work serves as an accessible foundation and outlook to recognize potential research gaps and define future directions. It identifies data modalities, such as time-series or graph data, and XAI methods that have not been extensively investigated for vulnerabilities in current research.
Cite as

Elisabeth Pachl, Fabian Langer, Thora Markert, and Jeanette Miriam Lorenz. A View on Vulnerabilites: The Security Challenges of XAI (Academic Track). In Symposium on Scaling AI Assessments (SAIA 2024). Open Access Series in Informatics (OASIcs), Volume 126, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pachl_et_al:OASIcs.SAIA.2024.12,
  author =	{Pachl, Elisabeth and Langer, Fabian and Markert, Thora and Lorenz, Jeanette Miriam},
  title =	{{A View on Vulnerabilites: The Security Challenges of XAI}},
  booktitle =	{Symposium on Scaling AI Assessments (SAIA 2024)},
  pages =	{12:1--12:23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-357-7},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{126},
  editor =	{G\"{o}rge, Rebekka and Haedecke, Elena and Poretschkin, Maximilian and Schmitz, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SAIA.2024.12},
  URN =		{urn:nbn:de:0030-drops-227523},
  doi =		{10.4230/OASIcs.SAIA.2024.12},
  annote =	{Keywords: Explainability, XAI, Transparency, Adversarial Machine Learning, Security, Vulnerabilities}
}
Document
DOI: 10.4230/DagRep.12.9.150
Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382)

Authors: Philipp Berens, Kyle Cranmer, Neil D. Lawrence, Ulrike von Luxburg, and Jessica Montgomery

Published in: Dagstuhl Reports, Volume 12, Issue 9 (2023)

Abstract
This report documents the programme and the outcomes of Dagstuhl Seminar 22382 "Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling". Today’s scientific challenges are characterised by complexity. Interconnected natural, technological, and human systems are influenced by forces acting across time- and spatial-scales, resulting in complex interactions and emergent behaviours. Understanding these phenomena - and leveraging scientific advances to deliver innovative solutions to improve society’s health, wealth, and well-being - requires new ways of analysing complex systems. The transformative potential of AI stems from its widespread applicability across disciplines, and will only be achieved through integration across research domains. AI for science is a rendezvous point. It brings together expertise from AI and application domains; combines modelling knowledge with engineering know-how; and relies on collaboration across disciplines and between humans and machines. Alongside technical advances, the next wave of progress in the field will come from building a community of machine learning researchers, domain experts, citizen scientists, and engineers working together to design and deploy effective AI tools. This report summarises the discussions from the seminar and provides a roadmap to suggest how different communities can collaborate to deliver a new wave of progress in AI and its application for scientific discovery.
Cite as

Philipp Berens, Kyle Cranmer, Neil D. Lawrence, Ulrike von Luxburg, and Jessica Montgomery. Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382). In Dagstuhl Reports, Volume 12, Issue 9, pp. 150-199, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{berens_et_al:DagRep.12.9.150,
  author =	{Berens, Philipp and Cranmer, Kyle and Lawrence, Neil D. and von Luxburg, Ulrike and Montgomery, Jessica},
  title =	{{Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382)}},
  pages =	{150--199},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{9},
  editor =	{Berens, Philipp and Cranmer, Kyle and Lawrence, Neil D. and von Luxburg, Ulrike and Montgomery, Jessica},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.9.150},
  URN =		{urn:nbn:de:0030-drops-178125},
  doi =		{10.4230/DagRep.12.9.150},
  annote =	{Keywords: machine learning, artificial intelligence, life sciences, physical sciences, environmental sciences, simulation, causality, modelling}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.18
On the Origins of Coccinelle

Authors: Julia Lawall

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Coccinelle is a program-transformation system for C code. It has been under development since 2005 and has been extensively used on the Linux kernel. The design of Coccinelle was inspired in part by the author’s previous experience in using Stratego/XT, developed by Eelco Visser. This paper reflects on some of Coccinelle’s design choices and their relation to Eelco Visser’s work.
Cite as

Julia Lawall. On the Origins of Coccinelle. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 18:1-18:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lawall:OASIcs.EVCS.2023.18,
  author =	{Lawall, Julia},
  title =	{{On the Origins of Coccinelle}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{18:1--18:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.18},
  URN =		{urn:nbn:de:0030-drops-177884},
  doi =		{10.4230/OASIcs.EVCS.2023.18},
  annote =	{Keywords: Linux kernel, Coccinelle, Stratego/XT, program transformation}
}
  • Refine by Type
  • 21 Document/PDF
  • 14 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 12 2025
  • 2 2023
  • 2 2019
  • 1 2014
  • Show More...

  • Refine by Author
  • 4 Lawall, Julia
  • 3 Muller, Gilles
  • 2 Barthe, Gilles
  • 2 Jiang, Lingxiao
  • 2 Kang, Hong Jin
  • Show More...

  • Refine by Series/Journal
  • 10 LIPIcs
  • 5 OASIcs
  • 1 DARTS
  • 1 LITES
  • 1 DagRep
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Logic and verification
  • 2 Computing methodologies → Machine learning
  • 2 Software and its engineering → Software maintenance tools
  • 2 Software and its engineering → Software notations and tools
  • 2 Theory of computation → Modal and temporal logics
  • Show More...

  • Refine by Keyword
  • 2 Java
  • 2 Mobility
  • 2 availability
  • 2 confidentiality
  • 2 cryptography
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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