56 Search Results for "R�glin, Heiko"

Document
Survey
DOI: 10.4230/TGDK.1.1.4
Knowledge Graph Embeddings: Open Challenges and Opportunities

Authors: Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
While Knowledge Graphs (KGs) have long been used as valuable sources of structured knowledge, in recent years, KG embeddings have become a popular way of deriving numeric vector representations from them, for instance, to support knowledge graph completion and similarity search. This study surveys advances as well as open challenges and opportunities in this area. For instance, the most prominent embedding models focus primarily on structural information. However, there has been notable progress in incorporating further aspects, such as semantics, multi-modal, temporal, and multilingual features. Most embedding techniques are assessed using human-curated benchmark datasets for the task of link prediction, neglecting other important real-world KG applications. Many approaches assume a static knowledge graph and are unable to account for dynamic changes. Additionally, KG embeddings may encode data biases and lack interpretability. Overall, this study provides an overview of promising research avenues to learn improved KG embeddings that can address a more diverse range of use cases.
Cite as

Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo. Knowledge Graph Embeddings: Open Challenges and Opportunities. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 4:1-4:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{biswas_et_al:TGDK.1.1.4,
  author =	{Biswas, Russa and Kaffee, Lucie-Aim\'{e}e and Cochez, Michael and Dumbrava, Stefania and Jendal, Theis E. and Lissandrini, Matteo and Lopez, Vanessa and Menc{\'\i}a, Eneldo Loza and Paulheim, Heiko and Sack, Harald and Vakaj, Edlira Kalemi and de Melo, Gerard},
  title =	{{Knowledge Graph Embeddings: Open Challenges and Opportunities}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:32},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.4},
  URN =		{urn:nbn:de:0030-drops-194783},
  doi =		{10.4230/TGDK.1.1.4},
  annote =	{Keywords: Knowledge Graphs, KG embeddings, Link prediction, KG applications}
}
Document
DOI: 10.4230/OASIcs.WCET.2023.4
Clustering Solutions of Multiobjective Function Inlining Problem

Authors: Kateryna Muts and Heiko Falk

Published in: OASIcs, Volume 114, 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)

Abstract
Hard real time-systems are often small devices operating on batteries that must react within a given deadline, so they must satisfy their timing, code size, and energy consumption requirements. Since these three objectives contradict each other, compilers for real-time systems go towards multiobjective optimizations which result in sets of trade-off solutions. A system designer can use the solution sets to choose the most suitable system configuration. Evolutionary algorithms can find trade-off solutions but the solution set might be large which complicates the task of the system designer. We propose to divide the solution set into clusters, so the system designer chooses the most suitable cluster and examines a smaller subset in detail. In contrast to other clustering techniques, our method guarantees that the sizes of all clusters are less than a predefined limit. Our method clusters a set by using any existing clustering method, divides clusters with sizes exceeding the predefined size into smaller clusters, and reduces the number of clusters by merging small clusters. The method guarantees that the final clusters satisfy the size constraint. We demonstrate our approach by considering a well-known compiler-based optimization called function inlining. It substitutes function calls by the function bodies which decreases the execution time and energy consumption of a program but increases its code size.
Cite as

Kateryna Muts and Heiko Falk. Clustering Solutions of Multiobjective Function Inlining Problem. In 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023). Open Access Series in Informatics (OASIcs), Volume 114, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{muts_et_al:OASIcs.WCET.2023.4,
  author =	{Muts, Kateryna and Falk, Heiko},
  title =	{{Clustering Solutions of Multiobjective Function Inlining Problem}},
  booktitle =	{21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)},
  pages =	{4:1--4:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-293-8},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{114},
  editor =	{W\"{a}gemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2023.4},
  URN =		{urn:nbn:de:0030-drops-184332},
  doi =		{10.4230/OASIcs.WCET.2023.4},
  annote =	{Keywords: Clustering, multiobjective optimization, compiler, hard real-time system}
}
Document
DOI: 10.4230/OASIcs.WCET.2023.5
Efficient and Effective Multi-Objective Optimization for Real-Time Multi-Task Systems

Authors: Shashank Jadhav and Heiko Falk

Published in: OASIcs, Volume 114, 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)

Abstract
Embedded real-time multi-task systems must often not only comply with timing constraints but also need to meet energy requirements. However, optimizing energy consumption might lead to higher Worst-Case Execution Time (WCET), leading to an un-schedulable system, as frequently executed code can easily differ from timing-critical code. To handle such an impasse in this paper, we formulate a Metaheuristic Algorithm-based Multi-objective Optimization (MAMO) for multi-task real-time systems. But, performing multiple WCET, energy, and schedulability analyses to solve a MAMO poses a bottleneck concerning compilation times. Therefore, we propose two novel approaches - Path-based Constraint Approach (PCA) and Impact-based Constraint Approach (ICA) - to reduce the solution search space size and to cope with this problem. Evaluations showed that PCA and ICA reduced compilation times by 85.31% and 77.31%, on average, over MAMO. For all the task sets, out of all solutions found by ICA-FPA, on average, 88.89% were on the final Pareto front.
Cite as

Shashank Jadhav and Heiko Falk. Efficient and Effective Multi-Objective Optimization for Real-Time Multi-Task Systems. In 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023). Open Access Series in Informatics (OASIcs), Volume 114, pp. 5:1-5:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jadhav_et_al:OASIcs.WCET.2023.5,
  author =	{Jadhav, Shashank and Falk, Heiko},
  title =	{{Efficient and Effective Multi-Objective Optimization for Real-Time Multi-Task Systems}},
  booktitle =	{21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)},
  pages =	{5:1--5:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-293-8},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{114},
  editor =	{W\"{a}gemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2023.5},
  URN =		{urn:nbn:de:0030-drops-184340},
  doi =		{10.4230/OASIcs.WCET.2023.5},
  annote =	{Keywords: Real-time systems, Multi-objective optimization, Metaheuristic algorithms, Compilers, Design space reduction}
}
Document
DOI: 10.4230/OASIcs.WCET.2023.6
Towards Multi-Objective Dynamic SPM Allocation

Authors: Shashank Jadhav and Heiko Falk

Published in: OASIcs, Volume 114, 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)

Abstract
Most real-time embedded systems are required to fulfill timing constraints while adhering to a limited energy budget. Small ScratchPad Memory (SPM) poses a common hardware constraint on embedded systems. Static SPM allocation techniques are limited by the SPM’s stringent size constraint, which is why this paper proposes a Dynamic SPM Allocation (DSA) model at the compiler level for the dynamic allocation of a program to SPM during runtime. To minimize Worst-Case Execution Time (WCET) and energy objectives, we propose a multi-objective DSA-based optimization. Static SPM allocations might inherently use SPM sub-optimally, while all proposed DSA optimizations are only single-objective. Therefore, this paper is the first step towards a DSA that trades WCET and energy objectives simultaneously. Even with extra DSA overheads, our approach provides better quality solutions than the state-of-the-art multi-objective static SPM allocation and ILP-based single-objective DSA approach.
Cite as

Shashank Jadhav and Heiko Falk. Towards Multi-Objective Dynamic SPM Allocation. In 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023). Open Access Series in Informatics (OASIcs), Volume 114, pp. 6:1-6:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jadhav_et_al:OASIcs.WCET.2023.6,
  author =	{Jadhav, Shashank and Falk, Heiko},
  title =	{{Towards Multi-Objective Dynamic SPM Allocation}},
  booktitle =	{21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)},
  pages =	{6:1--6:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-293-8},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{114},
  editor =	{W\"{a}gemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2023.6},
  URN =		{urn:nbn:de:0030-drops-184353},
  doi =		{10.4230/OASIcs.WCET.2023.6},
  annote =	{Keywords: Multi-objective optimization, Embedded systems, Compilers, Dynamic SPM allocation, Metaheuristic algorithms}
}
Document
DOI: 10.4230/OASIcs.WCET.2023.9
EnergyAnalyzer: Using Static WCET Analysis Techniques to Estimate the Energy Consumption of Embedded Applications

Authors: Simon Wegener, Kris K. Nikov, Jose Nunez-Yanez, and Kerstin Eder

Published in: OASIcs, Volume 114, 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)

Abstract
This paper presents EnergyAnalyzer, a code-level static analysis tool for estimating the energy consumption of embedded software based on statically predictable hardware events. The tool utilises techniques usually used for worst-case execution time (WCET) analysis together with bespoke energy models developed for two predictable architectures - the ARM Cortex-M0 and the Gaisler LEON3 - to perform energy usage analysis. EnergyAnalyzer has been applied in various use cases, such as selecting candidates for an optimised convolutional neural network, analysing the energy consumption of a camera pill prototype, and analysing the energy consumption of satellite communications software. The tool was developed as part of a larger project called TeamPlay, which aimed to provide a toolchain for developing embedded applications where energy properties are first-class citizens, allowing the developer to reflect directly on these properties at the source code level. The analysis capabilities of EnergyAnalyzer are validated across a large number of benchmarks for the two target architectures and the results show that the statically estimated energy consumption has, with a few exceptions, less than 1% difference compared to the underlying empirical energy models which have been validated on real hardware.
Cite as

Simon Wegener, Kris K. Nikov, Jose Nunez-Yanez, and Kerstin Eder. EnergyAnalyzer: Using Static WCET Analysis Techniques to Estimate the Energy Consumption of Embedded Applications. In 21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023). Open Access Series in Informatics (OASIcs), Volume 114, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wegener_et_al:OASIcs.WCET.2023.9,
  author =	{Wegener, Simon and Nikov, Kris K. and Nunez-Yanez, Jose and Eder, Kerstin},
  title =	{{EnergyAnalyzer: Using Static WCET Analysis Techniques to Estimate the Energy Consumption of Embedded Applications}},
  booktitle =	{21th International Workshop on Worst-Case Execution Time Analysis (WCET 2023)},
  pages =	{9:1--9:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-293-8},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{114},
  editor =	{W\"{a}gemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2023.9},
  URN =		{urn:nbn:de:0030-drops-184380},
  doi =		{10.4230/OASIcs.WCET.2023.9},
  annote =	{Keywords: Energy Modelling, Static Analysis, Gaisler LEON3, ARM Cortex-M0}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2023.50
Connected k-Center and k-Diameter Clustering

Authors: Lukas Drexler, Jan Eube, Kelin Luo, Heiko Röglin, Melanie Schmidt, and Julian Wargalla

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Motivated by an application from geodesy, we study the connected k-center problem and the connected k-diameter problem. These problems arise from the classical k-center and k-diameter problems by adding a side constraint. For the side constraint, we are given an undirected connectivity graph G on the input points, and a clustering is now only feasible if every cluster induces a connected subgraph in G. Usually in clustering problems one assumes that the clusters are pairwise disjoint. We study this case but additionally also the case that clusters are allowed to be non-disjoint. This can help to satisfy the connectivity constraints. Our main result is an O(1)-approximation algorithm for the disjoint connected k-center and k-diameter problem for Euclidean spaces of low dimension (constant d) and for metrics with constant doubling dimension. For general metrics, we get an O(log²k)-approximation. Our algorithms work by computing a non-disjoint connected clustering first and transforming it into a disjoint connected clustering. We complement these upper bounds by several upper and lower bounds for variations and special cases of the model.
Cite as

Lukas Drexler, Jan Eube, Kelin Luo, Heiko Röglin, Melanie Schmidt, and Julian Wargalla. Connected k-Center and k-Diameter Clustering. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 50:1-50:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{drexler_et_al:LIPIcs.ICALP.2023.50,
  author =	{Drexler, Lukas and Eube, Jan and Luo, Kelin and R\"{o}glin, Heiko and Schmidt, Melanie and Wargalla, Julian},
  title =	{{Connected k-Center and k-Diameter Clustering}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{50:1--50:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.50},
  URN =		{urn:nbn:de:0030-drops-181024},
  doi =		{10.4230/LIPIcs.ICALP.2023.50},
  annote =	{Keywords: Approximation algorithms, Clustering, Connectivity constraints}
}
Document
DOI: 10.4230/LIPIcs.ESA.2022.10
The Price of Hierarchical Clustering

Authors: Anna Arutyunova and Heiko Röglin

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
Hierarchical Clustering is a popular tool for understanding the hereditary properties of a data set. Such a clustering is actually a sequence of clusterings that starts with the trivial clustering in which every data point forms its own cluster and then successively merges two existing clusters until all points are in the same cluster. A hierarchical clustering achieves an approximation factor of α if the costs of each k-clustering in the hierarchy are at most α times the costs of an optimal k-clustering. We study as cost functions the maximum (discrete) radius of any cluster (k-center problem) and the maximum diameter of any cluster (k-diameter problem). In general, the optimal clusterings do not form a hierarchy and hence an approximation factor of 1 cannot be achieved. We call the smallest approximation factor that can be achieved for any instance the price of hierarchy. For the k-diameter problem we improve the upper bound on the price of hierarchy to 3+2√2≈ 5.83. Moreover we significantly improve the lower bounds for k-center and k-diameter, proving a price of hierarchy of exactly 4 and 3+2√2, respectively.
Cite as

Anna Arutyunova and Heiko Röglin. The Price of Hierarchical Clustering. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{arutyunova_et_al:LIPIcs.ESA.2022.10,
  author =	{Arutyunova, Anna and R\"{o}glin, Heiko},
  title =	{{The Price of Hierarchical Clustering}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2022.10},
  URN =		{urn:nbn:de:0030-drops-169487},
  doi =		{10.4230/LIPIcs.ESA.2022.10},
  annote =	{Keywords: Hierarchical Clustering, approximation Algorithms, k-center Problem}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.6
Dandelion: Certified Approximations of Elementary Functions

Authors: Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Elementary function operations such as sin and exp cannot in general be computed exactly on today’s digital computers, and thus have to be approximated. The standard approximations in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified. This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.
Cite as

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
  author =	{Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
  title =	{{Dandelion: Certified Approximations of Elementary Functions}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
  URN =		{urn:nbn:de:0030-drops-167155},
  doi =		{10.4230/LIPIcs.ITP.2022.6},
  annote =	{Keywords: elementary functions, approximation, certificate checking}
}
Document
DOI: 10.4230/OASIcs.WCET.2022.3
DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

Authors: Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke

Published in: OASIcs, Volume 103, 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)

Abstract
Constructing a complete control-flow graph (CGF) and computing upper bounds on loops of a computing system are essential to safely estimate the worst-case execution time (WCET) of real-time tasks. WCETs are required for verifying the timing requirements of a real-time computing system. Therefore, we propose an analysis using dynamic symbolic execution (DSE) that detects and computes upper bounds on the loops, and resolves indirect jumps. The proposed analysis constructs and initializes memory models, then it uses a satisfiability modulo theories (SMT) solver to symbolically execute the instructions. The analysis showed higher precision in bounding loops of the Mälardalen benchmarks comparing to SWEET and oRange. We integrated our analysis with the OTAWA toolbox for performing a WCET analysis. Then, we used the proposed analysis for estimating the WCET of functions in a use case inspired by an aerospace project.
Cite as

Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke. DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution. In 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022). Open Access Series in Informatics (OASIcs), Volume 103, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{abaza_et_al:OASIcs.WCET.2022.3,
  author =	{Abaza, Hazem and Haj Hammadeh, Zain Alabedin and L\"{u}dtke, Daniel},
  title =	{{DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution}},
  booktitle =	{20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)},
  pages =	{3:1--3:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-244-0},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{103},
  editor =	{Ballabriga, Cl\'{e}ment},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2022.3},
  URN =		{urn:nbn:de:0030-drops-166256},
  doi =		{10.4230/OASIcs.WCET.2022.3},
  annote =	{Keywords: Real-Time, WCET, Symbolic execution}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.10
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)

Authors: Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This document describes the artifact for RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{becker_et_al:DARTS.8.2.10,
  author =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  title =	{{Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.10},
  URN =		{urn:nbn:de:0030-drops-162086},
  doi =		{10.4230/DARTS.8.2.10},
  annote =	{Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.1
Verified Compilation and Optimization of Floating-Point Programs in CakeML

Authors: Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1:1-1:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ECOOP.2022.1,
  author =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  title =	{{Verified Compilation and Optimization of Floating-Point Programs in CakeML}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{1:1--1:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.1},
  URN =		{urn:nbn:de:0030-drops-162290},
  doi =		{10.4230/LIPIcs.ECOOP.2022.1},
  annote =	{Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2022.7
Minimum-Error Triangulations for Sea Surface Reconstruction

Authors: Anna Arutyunova, Anne Driemel, Jan-Henrik Haunert, Herman Haverkort, Jürgen Kusche, Elmar Langetepe, Philip Mayer, Petra Mutzel, and Heiko Röglin

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
We apply state-of-the-art computational geometry methods to the problem of reconstructing a time-varying sea surface from tide gauge records. Our work builds on a recent article by Nitzke et al. (Computers & Geosciences, 157:104920, 2021) who have suggested to learn a triangulation D of a given set of tide gauge stations. The objective is to minimize the misfit of the piecewise linear surface induced by D to a reference surface that has been acquired with satellite altimetry. The authors restricted their search to k-order Delaunay (k-OD) triangulations and used an integer linear program in order to solve the resulting optimization problem. In geometric terms, the input to our problem consists of two sets of points in ℝ² with elevations: a set 𝒮 that is to be triangulated, and a set ℛ of reference points. Intuitively, we define the error of a triangulation as the average vertical distance of a point in ℛ to the triangulated surface that is obtained by interpolating elevations of 𝒮 linearly in each triangle. Our goal is to find the triangulation of 𝒮 that has minimum error with respect to ℛ. In our work, we prove that the minimum-error triangulation problem is NP-hard and cannot be approximated within any multiplicative factor in polynomial time unless P = NP. At the same time we show that the problem instances that occur in our application (considering sea level data from several hundreds of tide gauge stations worldwide) can be solved relatively fast using dynamic programming when restricted to k-OD triangulations for k ≤ 7. In particular, instances for which the number of connected components of the so-called k-OD fixed-edge graph is small can be solved within few seconds.
Cite as

Anna Arutyunova, Anne Driemel, Jan-Henrik Haunert, Herman Haverkort, Jürgen Kusche, Elmar Langetepe, Philip Mayer, Petra Mutzel, and Heiko Röglin. Minimum-Error Triangulations for Sea Surface Reconstruction. In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{arutyunova_et_al:LIPIcs.SoCG.2022.7,
  author =	{Arutyunova, Anna and Driemel, Anne and Haunert, Jan-Henrik and Haverkort, Herman and Kusche, J\"{u}rgen and Langetepe, Elmar and Mayer, Philip and Mutzel, Petra and R\"{o}glin, Heiko},
  title =	{{Minimum-Error Triangulations for Sea Surface Reconstruction}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.7},
  URN =		{urn:nbn:de:0030-drops-160155},
  doi =		{10.4230/LIPIcs.SoCG.2022.7},
  annote =	{Keywords: Minimum-Error Triangulation, k-Order Delaunay Triangulations, Data dependent Triangulations, Sea Surface Reconstruction, fixed-Edge Graph}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.26
The Isomorphism Problem for Plain Groups Is in Σ₃^{𝖯}

Authors: Heiko Dietrich, Murray Elder, Adam Piggott, Youming Qiao, and Armin Weiß

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
Testing isomorphism of infinite groups is a classical topic, but from the complexity theory viewpoint, few results are known. Sénizergues and the fifth author (ICALP2018) proved that the isomorphism problem for virtually free groups is decidable in PSPACE when the input is given in terms of so-called virtually free presentations. Here we consider the isomorphism problem for the class of plain groups, that is, groups that are isomorphic to a free product of finitely many finite groups and finitely many copies of the infinite cyclic group. Every plain group is naturally and efficiently presented via an inverse-closed finite convergent length-reducing rewriting system. We prove that the isomorphism problem for plain groups given in this form lies in the polynomial time hierarchy, more precisely, in Σ₃^𝖯. This result is achieved by combining new geometric and algebraic characterisations of groups presented by inverse-closed finite convergent length-reducing rewriting systems developed in recent work of the second and third authors (2021) with classical finite group isomorphism results of Babai and Szemerédi (1984).
Cite as

Heiko Dietrich, Murray Elder, Adam Piggott, Youming Qiao, and Armin Weiß. The Isomorphism Problem for Plain Groups Is in Σ₃^{𝖯}. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 26:1-26:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dietrich_et_al:LIPIcs.STACS.2022.26,
  author =	{Dietrich, Heiko and Elder, Murray and Piggott, Adam and Qiao, Youming and Wei{\ss}, Armin},
  title =	{{The Isomorphism Problem for Plain Groups Is in \Sigma₃^\{𝖯\}}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{26:1--26:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.26},
  URN =		{urn:nbn:de:0030-drops-158368},
  doi =		{10.4230/LIPIcs.STACS.2022.26},
  annote =	{Keywords: plain group, isomorphism problem, polynomial hierarchy, \Sigma₃^\{𝖯\} complexity class, inverse-closed finite convergent length-reducing rewriting system}
}
Document
APPROX
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2021.18
Upper and Lower Bounds for Complete Linkage in General Metric Spaces

Authors: Anna Arutyunova, Anna Großwendt, Heiko Röglin, Melanie Schmidt, and Julian Wargalla

Published in: LIPIcs, Volume 207, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2021)

Abstract
In a hierarchical clustering problem the task is to compute a series of mutually compatible clusterings of a finite metric space (P,dist). Starting with the clustering where every point forms its own cluster, one iteratively merges two clusters until only one cluster remains. Complete linkage is a well-known and popular algorithm to compute such clusterings: in every step it merges the two clusters whose union has the smallest radius (or diameter) among all currently possible merges. We prove that the radius (or diameter) of every k-clustering computed by complete linkage is at most by factor O(k) (or O(k²)) worse than an optimal k-clustering minimizing the radius (or diameter). Furthermore we give a negative answer to the question proposed by Dasgupta and Long [Sanjoy Dasgupta and Philip M. Long, 2005], who show a lower bound of Ω(log(k)) and ask if the approximation guarantee is in fact Θ(log(k)). We present instances where complete linkage performs poorly in the sense that the k-clustering computed by complete linkage is off by a factor of Ω(k) from an optimal solution for radius and diameter. We conclude that in general metric spaces complete linkage does not perform asymptotically better than single linkage, merging the two clusters with smallest inter-cluster distance, for which we prove an approximation guarantee of O(k).
Cite as

Anna Arutyunova, Anna Großwendt, Heiko Röglin, Melanie Schmidt, and Julian Wargalla. Upper and Lower Bounds for Complete Linkage in General Metric Spaces. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 207, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{arutyunova_et_al:LIPIcs.APPROX/RANDOM.2021.18,
  author =	{Arutyunova, Anna and Gro{\ss}wendt, Anna and R\"{o}glin, Heiko and Schmidt, Melanie and Wargalla, Julian},
  title =	{{Upper and Lower Bounds for Complete Linkage in General Metric Spaces}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2021)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-207-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{207},
  editor =	{Wootters, Mary and Sanit\`{a}, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2021.18},
  URN =		{urn:nbn:de:0030-drops-147115},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2021.18},
  annote =	{Keywords: Hierarchical Clustering, Complete Linkage, agglomerative Clustering, k-Center}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2021.II.6
Bicriteria Aggregation of Polygons via Graph Cuts

Authors: Peter Rottmann, Anne Driemel, Herman Haverkort, Heiko Röglin, and Jan-Henrik Haunert

Published in: LIPIcs, Volume 208, 11th International Conference on Geographic Information Science (GIScience 2021) - Part II

Abstract
We present a new method for the task of detecting groups of polygons in a given geographic data set and computing a representative polygon for each group. This task is relevant in map generalization where the aim is to derive a less detailed map from a given map. Following a classical approach, we define the output polygons by merging the input polygons with a set of triangles that we select from a constrained Delaunay triangulation of the input polygons' exterior. The innovation of our method is to compute the selection of triangles by solving a bicriteria optimization problem. While on the one hand we aim at minimizing the total area of the outputs polygons, we aim on the other hand at minimizing their total perimeter. We combine these two objectives in a weighted sum and study two computational problems that naturally arise. In the first problem, the parameter that balances the two objectives is fixed and the aim is to compute a single optimal solution. In the second problem, the aim is to compute a set containing an optimal solution for every possible value of the parameter. We present efficient algorithms for these problems based on computing a minimum cut in an appropriately defined graph. Moreover, we show how the result set of the second problem can be approximated with few solutions. In an experimental evaluation, we finally show that the method is able to derive settlement areas from building footprints that are similar to reference solutions.
Cite as

Peter Rottmann, Anne Driemel, Herman Haverkort, Heiko Röglin, and Jan-Henrik Haunert. Bicriteria Aggregation of Polygons via Graph Cuts. In 11th International Conference on Geographic Information Science (GIScience 2021) - Part II. Leibniz International Proceedings in Informatics (LIPIcs), Volume 208, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{rottmann_et_al:LIPIcs.GIScience.2021.II.6,
  author =	{Rottmann, Peter and Driemel, Anne and Haverkort, Herman and R\"{o}glin, Heiko and Haunert, Jan-Henrik},
  title =	{{Bicriteria Aggregation of Polygons via Graph Cuts}},
  booktitle =	{11th International Conference on Geographic Information Science (GIScience 2021) - Part II},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-208-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{208},
  editor =	{Janowicz, Krzysztof and Verstegen, Judith A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2021.II.6},
  URN =		{urn:nbn:de:0030-drops-147658},
  doi =		{10.4230/LIPIcs.GIScience.2021.II.6},
  annote =	{Keywords: map generalization, aggregation, graph cuts, bicriteria optimization}
}
  • Refine by Author
  • 11 Falk, Heiko
  • 11 Röglin, Heiko
  • 5 Mantel, Heiko
  • 5 Sabelfeld, Andrei
  • 3 Arutyunova, Anna
  • Show More...

  • Refine by Classification
  • 6 Software and its engineering → Compilers
  • 4 Computer systems organization → Real-time systems
  • 4 Theory of computation → Facility location and clustering
  • 3 Mathematics of computing → Discrete mathematics
  • 3 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 5 WCET
  • 4 information flow
  • 3 Real-Time Systems
  • 3 WCET analysis
  • 3 compiler
  • Show More...

  • Refine by Type
  • 56 document

  • Refine by Publication Year
  • 13 2014
  • 7 2022
  • 6 2023
  • 3 2006
  • 3 2021
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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