15 Search Results for "Rinard, Martin"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.18
Iterating Non-Aggregative Structure Compositions

Authors: Marius Bozga, Radu Iosif, and Florian Zuleger

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called fusion, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite hyperedge-replacement (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called context-free. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.
Cite as

Marius Bozga, Radu Iosif, and Florian Zuleger. Iterating Non-Aggregative Structure Compositions. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.FSTTCS.2025.18,
  author =	{Bozga, Marius and Iosif, Radu and Zuleger, Florian},
  title =	{{Iterating Non-Aggregative Structure Compositions}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.18},
  URN =		{urn:nbn:de:0030-drops-250997},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.18},
  annote =	{Keywords: Hyperedge replacement, Tree-width}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.1
A Certified Proof Checker for Deep Neural Network Verification in Imandra

Authors: Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz

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

Abstract
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra - an industrial functional programming language and an interactive theorem prover (ITP) - that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.
Cite as

Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desmartin_et_al:LIPIcs.ITP.2025.1,
  author =	{Desmartin, Remi and Isac, Omri and Passmore, Grant and Komendantskaya, Ekaterina and Stark, Kathrin and Katz, Guy},
  title =	{{A Certified Proof Checker for Deep Neural Network Verification in Imandra}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{1:1--1:21},
  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.1},
  URN =		{urn:nbn:de:0030-drops-246000},
  doi =		{10.4230/LIPIcs.ITP.2025.1},
  annote =	{Keywords: Neural Network Verification, Farkas Lemma, Proof Certification}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.6
Exploration and Complexity Management in Graph-Based Programming Environments

Authors: Max Boksem and L. Thomas van Binsbergen

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

Abstract
Programmers often rely on different environments depending on the nature of their tasks. For large-scale software projects, IDEs help manage complexity through structured abstractions like files, modules, and classes, and provide tools for code visualization and navigation. In contrast, exploratory programming tasks - such as data analysis, rapid prototyping, and design space exploration - are better served by interactive environments like REPLs and Notebooks, which support incremental development and immediate feedback. However, these tools tend to prioritize either complexity management or exploration, limiting their effectiveness across contexts. This paper investigates a hybrid graph-based programming environment that bridges these two modes by building on Incremental Graph Code (IGC), a graph-based system for structuring, visualizing, and interacting with source code. We explore how IGC can support both complexity management and exploratory programming through three key features: projectional views for aggregating and navigating interrelated code and documentation, graph-type nodes for encapsulating subgraphs to manage structural complexity, and an exploratory programming view for managing branching executions and promoting experimentation. Together, these features suggest that graph-based environments like IGC can offer a unified platform for both systematic software engineering and dynamic, exploratory development.
Cite as

Max Boksem and L. Thomas van Binsbergen. Exploration and Complexity Management in Graph-Based Programming Environments. 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. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{boksem_et_al:OASIcs.Programming.2025.6,
  author =	{Boksem, Max and van Binsbergen, L. Thomas},
  title =	{{Exploration and Complexity Management in Graph-Based Programming Environments}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{6:1--6:18},
  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.6},
  URN =		{urn:nbn:de:0030-drops-242906},
  doi =		{10.4230/OASIcs.Programming.2025.6},
  annote =	{Keywords: Graph-based Programming Environments, Exploratory Programming, Complexity Management, Incremental Graph Code (IGC), Projectional Views}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.8
Fuzzing as Editor Feedback

Authors: Marcel Garus, Jens Lincke, and Robert Hirschfeld

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

Abstract
Live programming requires concrete examples, but coming up with examples takes effort. However, there are ways to execute code without specifying examples, such as fuzzing. Fuzzing is a technique that synthesizes program inputs to find bugs in security-critical software. While fuzzing focuses on finding crashes, it also produces valid inputs as a byproduct. Our approach is to make use of this to show examples, including edge cases, directly in the editor. To provide examples for individual pieces of code, we implement fuzzing at the granularity of functions. We integrate it into the compiler pipeline and language tooling of Martinaise, a custom programming language with a limited feature set. Initially, our examples are random and then mutate based on coverage feedback to reach interesting code locations and become smaller. We evaluate our tool in small case studies, showing generated examples for numbers, strings, and composite objects. Our fuzzed examples still feel synthetic, but since they are grounded in the dynamic behavior of code, they can cover the entire execution and show edge cases.
Cite as

Marcel Garus, Jens Lincke, and Robert Hirschfeld. Fuzzing as Editor Feedback. 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. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{garus_et_al:OASIcs.Programming.2025.8,
  author =	{Garus, Marcel and Lincke, Jens and Hirschfeld, Robert},
  title =	{{Fuzzing as Editor Feedback}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{8:1--8: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.8},
  URN =		{urn:nbn:de:0030-drops-242926},
  doi =		{10.4230/OASIcs.Programming.2025.8},
  annote =	{Keywords: Fuzzing, Example-based Programming, Babylonian Programming, Dynamic Analysis, Code Coverage, Randomized Testing, Function-Level Fuzzing}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.13
Dimensions of Examples: Toward a Framework for Qualifying Examples in Programming

Authors: Toni Mattis, Lukas Böhme, Stefan Ramson, Tom Beckmann, Martin C. Rinard, and Robert Hirschfeld

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

Abstract
Programming requires understanding, using, and changing abstract source code and other representations of programs. Concrete examples demonstrate a particular instance of their abstract behavior. Hence, they play an important role in program comprehension, specification, and testing of requirements. Authoring examples entails a range of - often implicit - decisions about the content and presentation of the example. In this work, we attempt to structure this decision space by describing a set of dimensions that characterize examples in programming. As the manual effort of creating examples is increasingly automated, e.g., through the use of generative AI, we expect this catalog of dimensions to help users and tool developers parametrize, guide, and evaluate the generation of examples in terms of the vocabulary we present here.
Cite as

Toni Mattis, Lukas Böhme, Stefan Ramson, Tom Beckmann, Martin C. Rinard, and Robert Hirschfeld. Dimensions of Examples: Toward a Framework for Qualifying Examples in Programming. 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. 13:1-13:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mattis_et_al:OASIcs.Programming.2025.13,
  author =	{Mattis, Toni and B\"{o}hme, Lukas and Ramson, Stefan and Beckmann, Tom and Rinard, Martin C. and Hirschfeld, Robert},
  title =	{{Dimensions of Examples: Toward a Framework for Qualifying Examples in Programming}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{13:1--13:11},
  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.13},
  URN =		{urn:nbn:de:0030-drops-242973},
  doi =		{10.4230/OASIcs.Programming.2025.13},
  annote =	{Keywords: Examples, Live Programming, Evaluation}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.15
Encouraging Experimentation Through Programming by Proximity

Authors: Tom Beckmann, Leonard Geier, Stefan Ramson, Marcel Taeumel, and Robert Hirschfeld

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

Abstract
Exploratory programming involves evaluating a variety of approaches to identify those that advance the problem understanding. For this purpose, we investigated a notation for code designed to encourage experimentation with elements of a program. In our proof-of-concept, we evaluate the idea of program elements connecting by mere proximity through small case studies. We identify multiple constraints to enable connection through proximity and its limitations.
Cite as

Tom Beckmann, Leonard Geier, Stefan Ramson, Marcel Taeumel, and Robert Hirschfeld. Encouraging Experimentation Through Programming by Proximity. 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. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beckmann_et_al:OASIcs.Programming.2025.15,
  author =	{Beckmann, Tom and Geier, Leonard and Ramson, Stefan and Taeumel, Marcel and Hirschfeld, Robert},
  title =	{{Encouraging Experimentation Through Programming by Proximity}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{15:1--15: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.15},
  URN =		{urn:nbn:de:0030-drops-242991},
  doi =		{10.4230/OASIcs.Programming.2025.15},
  annote =	{Keywords: Visual Programming, Proximity, Experimentation Support}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.32
Efficient Certified Reasoning for Binarized Neural Networks

Authors: Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Neural networks have emerged as essential components in safety-critical applications - these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios. In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a 9× speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a 218× speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for 99% and 86% of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only 62% and 4% of the queries, respectively.
Cite as

Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Efficient Certified Reasoning for Binarized Neural Networks. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2025.32,
  author =	{Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
  title =	{{Efficient Certified Reasoning for Binarized Neural Networks}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
  URN =		{urn:nbn:de:0030-drops-237665},
  doi =		{10.4230/LIPIcs.SAT.2025.32},
  annote =	{Keywords: Neural network verification, proof certification, SAT solving, approximate model counting}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.2
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk)

Authors: Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

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

Abstract
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the "neural" and "symbolic" program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle - standing as an abbreviation for a "verification condition language" - an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle’s overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.
Cite as

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{daggitt_et_al:LIPIcs.FSCD.2025.2,
  author =	{Daggitt, Matthew L. and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca},
  title =	{{Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{2:1--2:20},
  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.2},
  URN =		{urn:nbn:de:0030-drops-236172},
  doi =		{10.4230/LIPIcs.FSCD.2025.2},
  annote =	{Keywords: Neural Network Verification, Types, Interactive Theorem Provers}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.19
Profile-Guided Field Externalization in an Ahead-Of-Time Compiler

Authors: Sebastian Kloibhofer, Lukas Makor, Peter Hofer, David Leopoldseder, and Hanspeter Mössenböck

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

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
DOI: 10.4230/LIPIcs.ECOOP.2025.21
GSOHC: Global Synchronization Optimization in Heterogeneous Computing

Authors: Soumik Kumar Basu and Jyothi Vedurada

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

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
DOI: 10.4230/LIPIcs.CSL.2025.9
On Homogeneous Models of Fluted Languages

Authors: Daumantas Kojelis

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of "nice" models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is Tower-complete. If only two variable are used, computational complexity drops to NExpTime-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, Σ⁰₁- and Π⁰₁-complete. Additionally, satisfiability becomes Σ¹₁-complete if periodic counting quantifiers are permitted.
Cite as

Daumantas Kojelis. On Homogeneous Models of Fluted Languages. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kojelis:LIPIcs.CSL.2025.9,
  author =	{Kojelis, Daumantas},
  title =	{{On Homogeneous Models of Fluted Languages}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.9},
  URN =		{urn:nbn:de:0030-drops-227669},
  doi =		{10.4230/LIPIcs.CSL.2025.9},
  annote =	{Keywords: Fluted Fragment, Fluted Logic, Fluted Fragment with Periodic Counting, Adjacent Fragment, Adjacent Fragment with Counting, Adjacent Fragment with Periodic Counting, Counting Quantifiers, Periodic Counting Quantifiers, Decidable Fragments of First-Order Logic}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.9
A Concurrent Language for Argumentation: Preliminary Notes

Authors: Stefano Bistarelli and Carlo Taticchi

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
While agent-based modelling languages naturally implement concurrency, the currently available languages for argumentation do not allow to explicitly model this type of interaction. In this paper we introduce a concurrent language for handling process arguing and communicating using a shared argumentation framework (reminding shared constraint store as in concurrent constraint). We introduce also basic expansions, contraction and revision procedures as main bricks for enforcement, debate, negotiation and persuasion.
Cite as

Stefano Bistarelli and Carlo Taticchi. A Concurrent Language for Argumentation: Preliminary Notes. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bistarelli_et_al:OASIcs.Gabbrielli.9,
  author =	{Bistarelli, Stefano and Taticchi, Carlo},
  title =	{{A Concurrent Language for Argumentation: Preliminary Notes}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{9:1--9:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.9},
  URN =		{urn:nbn:de:0030-drops-132311},
  doi =		{10.4230/OASIcs.Gabbrielli.9},
  annote =	{Keywords: Argumentation, Concurrent Language, Debating, Negotiation, Belief Revision}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.11
Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy

Authors: Moreno Falaschi, Catuscia Palamidessi, and Marco Romanelli

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
This paper shows how we can combine the power of machine learning with the flexibility of constraints. More specifically, we show how machine learning models can be represented by first-order logic theories, and how to derive these theories. The advantage of this representation is that it can be augmented with additional formulae, representing constraints of some kind on the data domain. For instance, new knowledge, or potential attackers, or fairness desiderata. We consider various kinds of learning algorithms (neural networks, k-nearest-neighbours, decision trees, support vector machines) and for each of them we show how to infer the FOL formulae. Then we focus on one particular application domain, namely the field of security and privacy. The idea is to represent the potentialities and goals of the attacker as a set of constraints, then use a constraint solver (more precisely, a solver modulo theories) to verify the satisfiability. If a solution exists, then it means that an attack is possible, otherwise, the system is safe. We show various examples from different areas of security and privacy; specifically, we consider a side-channel attack on a password checker, a malware attack on smart health systems, and a model-inversion attack on a neural network.
Cite as

Moreno Falaschi, Catuscia Palamidessi, and Marco Romanelli. Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{falaschi_et_al:OASIcs.Gabbrielli.11,
  author =	{Falaschi, Moreno and Palamidessi, Catuscia and Romanelli, Marco},
  title =	{{Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{11:1--11:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.11},
  URN =		{urn:nbn:de:0030-drops-132338},
  doi =		{10.4230/OASIcs.Gabbrielli.11},
  annote =	{Keywords: Constraints, machine learning, privacy, security}
}
Document
DOI: 10.4230/DagRep.1.2.16
Self-Repairing Programs (Dagstuhl Seminar 11062)

Authors: Mauro Pezzè, Martin C. Rinard, Westley Weimer, and Andreas Zeller

Published in: Dagstuhl Reports, Volume 1, Issue 2 (2011)

Abstract
Dagstuhl seminar 11062 ``Self-Repairing Programs'' included 23 participants and organizers from research and industrial communities. Self-Repairing Programs are a new and emerging area, and many participants reported that they initially felt their first research home to be in another area, such as testing, program synthesis, debugging, self-healing systems, or security. Over the course of the seminar, the participants found common ground in discussions of concerns, challenges, and the state of the art.
Cite as

Mauro Pezzè, Martin C. Rinard, Westley Weimer, and Andreas Zeller. Self-Repairing Programs (Dagstuhl Seminar 11062). In Dagstuhl Reports, Volume 1, Issue 2, pp. 16-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{pezze_et_al:DagRep.1.2.16,
  author =	{Pezz\`{e}, Mauro and Rinard, Martin C. and Weimer, Westley and Zeller, Andreas},
  title =	{{Self-Repairing Programs (Dagstuhl Seminar 11062)}},
  pages =	{16--29},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{2},
  editor =	{Pezz\`{e}, Mauro and Rinard, Martin C. and Weimer, Westley and Zeller, Andreas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.2.16},
  URN =		{urn:nbn:de:0030-drops-31525},
  doi =		{10.4230/DagRep.1.2.16},
  annote =	{Keywords: Automated program repair, contract, debugging, fault, patch, self-healing}
}
Document
DOI: 10.4230/DagSemProc.05431.4
On Algorithms and Complexity for Sets with Cardinality Constraints

Authors: Viktor Kuncak, Martin Rinard, and Bruno Marnette

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
Complexity of data structures in modern programs presents a challenge for current analysis and verification tools, forcing them to report false alarms or miss errors. I will describe a new approach for verifying programs with complex data structures. This approach builds on program analysis techniques, as well as decision procedures and theorem provers. The approach is based on specifying interfaces of data structures by writing procedure preconditions and postconditions in terms of abstract sets and relations. Our system then separately verifies that 1) each data structure conforms to its interface, 2) each data structure interface is used correctly, and 3) desired high-level application-specific invariants hold. The system verifies these conditions by combining decision procedures, theorem provers, and static analyses, promising an unprecedented tradeoff between precision and scalability. In the context of this system, we have developed new decision procedures for reasoning about sets and their cardinalities, approaches for extending the applicability of existing decision procedures, and techniques for modular analysis of dynamically created data structure instances.
Cite as

Viktor Kuncak, Martin Rinard, and Bruno Marnette. On Algorithms and Complexity for Sets with Cardinality Constraints. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kuncak_et_al:DagSemProc.05431.4,
  author =	{Kuncak, Viktor and Rinard, Martin and Marnette, Bruno},
  title =	{{On Algorithms and Complexity for Sets with Cardinality Constraints}},
  booktitle =	{Deduction and Applications},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.4},
  URN =		{urn:nbn:de:0030-drops-5125},
  doi =		{10.4230/DagSemProc.05431.4},
  annote =	{Keywords: Static analysis, data structure consistency, program verification, decision procedures}
}
  • Refine by Type
  • 15 Document/PDF
  • 11 Document/HTML

  • Refine by Publication Year
  • 11 2025
  • 2 2020
  • 1 2011
  • 1 2006

  • Refine by Author
  • 3 Hirschfeld, Robert
  • 2 Beckmann, Tom
  • 2 Komendantskaya, Ekaterina
  • 2 Ramson, Stefan
  • 2 Rinard, Martin C.
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 6 OASIcs
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 3 Computing methodologies → Neural networks
  • 2 Software and its engineering → Compilers
  • 2 Software and its engineering → Formal software verification
  • 2 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 2 Neural Network Verification
  • 1 Adjacent Fragment
  • 1 Adjacent Fragment with Counting
  • 1 Adjacent Fragment with Periodic Counting
  • 1 Argumentation
  • 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