1,497 Works

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Chad E. Brown, Cezary Kaliszyk & Karol Pak
We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and...

Algorithms, Bounds, and Strategies for Entangled XOR Games

Adam Bene Watts, Aram W. Harrow, Gurtej Kanwar & Anand Natarajan
Entangled games are a quantum analog of constraint satisfaction problems and have had important applications to quantum complexity theory, quantum cryptography, and the foundations of quantum mechanics. Given a game, the basic computational problem is to compute its entangled value: the supremum success probability attainable by a quantum strategy. We study the complexity of computing the (commuting-operator) entangled value omega^* of entangled XOR games with any number of players. Based on a duality theory for...

SPARQL Query Recommendation by Example: Assessing the Impact of Structural Analysis on Star-Shaped Queries

Alessandro Adamou, Carlo Allocca, Mathieu D'Aquin & Enrico Motta
One of the existing query recommendation strategies for unknown datasets is "by example", i.e. based on a query that the user already knows how to formulate on another dataset within a similar domain. In this paper we measure what contribution a structural analysis of the query and the datasets can bring to a recommendation strategy, to go alongside approaches that provide a semantic analysis. Here we concentrate on the case of star-shaped SPARQL queries over...

Minimum-Width Double-Strip and Parallelogram Annulus

Sang Won Bae
In this paper, we study the problem of computing a minimum-width double-strip or parallelogram annulus that encloses a given set of n points in the plane. A double-strip is a closed region in the plane whose boundary consists of four parallel lines and a parallelogram annulus is a closed region between two edge-parallel parallelograms. We present several first algorithms for these problems. Among them are O(n^2) and O(n^3 log n)-time algorithms that compute a minimum-width...

Front Matter, Table of Contents, Preface, Conference Organization

Jukka Suomela
Front Matter, Table of Contents, Preface, Conference Organization

Programmable Network Data Planes (Dagstuhl Seminar 19141)

Gianni Antichi, Theophilus Benson, Nate Foster, Fernando M. V. Ramos & Justine Sherry
Software-Defined Networking (SDN) started the "softwarization" of networking. By relocating the control plane onto a logically centralized machine, SDN gave programmers the ability to specify the behavior of the network directly in software, unleashing a major transformation both in the networking research community and in industry. However, a key limitation of the original SDN vision was the limited functionality exposed in protocols such as OpenFlow. Recent efforts to develop reconfigurable data planes and high-level network...

Computational Proteomics (Dagstuhl Seminar 19351)

Nuno Bandeira & Lennart Martens
This report documents the program and the outcomes of Dagstuhl Seminar 19351 ``Computational Proteomics''. The Seminar was originally built around four topics, identification and quantification of DIA data; algorithms for the analysis of protein cross-linking data; creating an online view on complete, browsable proteomes from public data; and detecting interesting biology from proteomics findings. These four topics were led to four correpsonding breakout sessions, which in turn led to five offshoot breakout sessions. The abstracts...

Computation in Low-Dimensional Geometry and Topology (Dagstuhl Seminar 19352)

Maartten Löffler, Anna Lubiw, Saul Schleimer & Erin Moriarty Wolf Chambers
This report documents the program and the outcomes of Dagstuhl Seminar 19352 ``Computation in Low-Dimensional Geometry and Topology''. The seminar participants investigated problems in: knot theory, trajectory analysis, algorithmic topology, computational geometry of curves, and graph drawing, with an emphasis on how low-dimensional structures change over time.

Advances and Challenges in Protein-RNA Recognition, Regulation and Prediction (Dagstuhl Seminar 19342)

Rolf Backofen, Yael Mandel-Gutfreund, Uwe Ohler & Gabriele Varani
This report documents the program and the outcomes of Dagstuhl Seminar 19342 ``Advances and Challenges in Protein-RNA Recognition, Regulation and Prediction''.

Algorithms and Complexity for Continuous Problems (Dagstuhl Seminar 19341)

Dmitriy Bilyk, Aicke Hinrichs, Frances Y. Kuo & Klaus Ritter
From 18.08. to 23.08.2019, the Dagstuhl Seminar 19341 Algorithms and Complexity for Continuous Problems was held in the International Conference and Research Center (LZI), Schloss Dagstuhl. During the seminar, participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar can be found in this report. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are...

Software Protection Decision Support and Evaluation Methodologies (Dagstuhl Seminar 19331)

Bjorn De Sutter, Christian Collberg & Mila Dalla Preda
This report documents the program and the outcomes of Dagstuhl Seminar 19331 ``Software Protection Decision Support and Evaluation Methodologies''. The seminar is situated in the domain of software protection against so-called man-at-the-end attacks, in which attackers have white-box access to the software that embeds valuable assets with security requirements such as confidentiality and integrity. The attackers try to compromise those by reverse-engineering the software and by tampering with it. Within this domain, the seminar focused...

Deleting Edges to Restrict the Size of an Epidemic in Temporal Networks

Jessica Enright, Kitty Meeks, George B. Mertzios & Viktor Zamaraev
Spreading processes on graphs are a natural model for a wide variety of real-world phenomena, including information or behaviour spread over social networks, biological diseases spreading over contact or trade networks, and the potential flow of goods over logistical infrastructure. Often, the networks over which these processes spread are dynamic in nature, and can be modeled with graphs whose structure is subject to discrete changes over time, i.e. with temporal graphs. Here, we consider temporal...

Mobile Data Visualization (Dagstuhl Seminar 19292)

Eun Kyoung Choe, Raimund Dachselt, Petra Isenberg & Bongshin Lee
Mobile visualization is becoming more prevalent, and new mobile device form factors and hardware capabilities will continually emerge in the coming years. Therefore, it is timely to reflect on what has been discovered to date and to look into the future. This Dagstuhl seminar brought together both established and junior researchers, designers, and practitioners from relevant application and research fields, including visualization, ubiquitous computing, human-computer interaction, and health informatics. Five demos and five tutorials gave...

Cybersafety Threats - from Deception to Aggression (Dagstuhl Seminar 19302)

Zinaida Benenson, Marianne Junger, Daniela Oliveira & Gianluca Stringhini
A number of malicious activities, such as cyberbullying, disinformation, and phishing, are becoming increasingly serious, affecting the wellbeing of Internet users both financially and psychologically. These malicious activities are inherently socio-technical, and therefore effective countermeasures against them must draw not only from engineering and computer science, but also from other disciplines. To discuss these topics and find appropriate countermeasures, we assembled a group of researchers from a number of disciplines such as computer science, criminology,...

Secure Composition for Hardware Systems (Dagstuhl Seminar 19301)

Divya Arora, Ilia Polian, Francesco Regazzoni & Patrick Schaumont
The goal of the Dagstuhl Seminar 19301 ``Secure Composition for Hardware System'' was to establish a common understanding of principles and techniques that can facilitate composition and integration of hardware systems to achieve specified security guarantees. Theoretical foundations of secure composition have been laid out in the past, but they are limited to software systems. New and unique security challenges arise when a real system composed of a range of hardware components, including application-specific blocks,...

Data Series Management (Dagstuhl Seminar 19282)

Anthony Bagnall, Richard L. Cole, Themis Palpanas & Kostas Zoumpatianos
We now witness a very strong interest by users across different domains on data series (a.k.a. time series) management. It is not unusual for industrial applications that produce data series to involve numbers of sequences (or subsequences) in the order of billions (i.e., multiple TBs). As a result, analysts are unable to handle the vast amounts of data series that they have to manage and process. The goal of this seminar is to enable researchers...

Values in Computing (Dagstuhl Seminar 19291)

Christoph Becker, Gregor Engels, Andrew Feenberg, Maria Angela Ferrario & Geraldine Fitzpatrick
Values are deeply held principles guiding decisions of individuals, groups and organizations. Computing technologies are inevitably affected by values: through their design, values become embodied and enacted. However, some values are easier to quantify and articulate than others; for example, the financial value of a software product is easier to measure than its `fairness'. As a result, less measurable values are often dismissed in decision making processes as lacking evidence. This is particularly problematic since...

Notional Machines and Programming Language Semantics in Education (Dagstuhl Seminar 19281)

Mark Guzdial, Shriram Krishnamurthi, Juha Sorva & Jan Vahrenhold
A formal semantics of a language serves many purposes. It can help debug the language's design, be used to prove type soundness, and guide optimizers to confirm that their work is correctness-preserving. Formal semantics are evaluated by several criteria: full abstraction, adequacy, soundness and completeness, faithfulness to an underlying implementation, and so on. Unfortunately, we know relatively little about how non-experts, such as students, actually employ a semantics. Which models are they able to grasp?...

A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic

Quentin Peyras, Julien Brunel & David Chemouil
First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments...

Efficient Approximation Schemes for Uniform-Cost Clustering Problems in Planar Graphs

Vincent Cohen-Addad, Marcin Pilipczuk & Michal Pilipczuk
We consider the k-Median problem on planar graphs: given an edge-weighted planar graph G, a set of clients C subseteq V(G), a set of facilities F subseteq V(G), and an integer parameter k, the task is to find a set of at most k facilities whose opening minimizes the total connection cost of clients, where each client contributes to the cost with the distance to the closest open facility. We give two new approximation schemes...

Local Computation Algorithms for Spanners

Merav Parter, Ronitt Rubinfeld, Ali Vakilian & Anak Yodpinyanee
A graph spanner is a fundamental graph structure that faithfully preserves the pairwise distances in the input graph up to a small multiplicative stretch. The common objective in the computation of spanners is to achieve the best-known existential size-stretch trade-off efficiently. Classical models and algorithmic analysis of graph spanners essentially assume that the algorithm can read the input graph, construct the desired spanner, and write the answer to the output tape. However, when considering massive...

Sketching Graphs and Combinatorial Optimization (Invited Talk)

Robert Krauthgamer
Graph-sketching algorithms summarize an input graph G in a manner that suffices to later answer (perhaps approximately) one or more optimization problems on G, like distances, cuts, and matchings. Two famous examples are the Gomory-Hu tree, which represents all the minimum st-cuts in a graph G using a tree on the same vertex set V(G); and the cut-sparsifier of Benczúr and Karger, which is a sparse graph (often a reweighted subgraph) that approximates every cut...

Large-Scale Distributed Algorithms for Facility Location with Outliers

Tanmay Inamdar, Shreyas Pai & Sriram V. Pemmaraju
This paper presents fast, distributed, O(1)-approximation algorithms for metric facility location problems with outliers in the Congested Clique model, Massively Parallel Computation (MPC) model, and in the k-machine model. The paper considers Robust Facility Location and Facility Location with Penalties, two versions of the facility location problem with outliers proposed by Charikar et al. (SODA 2001). The paper also considers two alternatives for specifying the input: the input metric can be provided explicitly (as an...

Counting Induced Subgraphs: An Algebraic Approach to #W[1]-hardness

Julian Dörfler, Marc Roth, Johannes Schmitt & Philip Wellnitz
We study the problem #IndSub(Phi) of counting all induced subgraphs of size k in a graph G that satisfy the property Phi. This problem was introduced by Jerrum and Meeks and shown to be #W[1]-hard when parameterized by k for some families of properties Phi including, among others, connectivity [JCSS 15] and even- or oddness of the number of edges [Combinatorica 17]. Very recently [IPEC 18], two of the authors introduced a novel technique for...

NumLin: Linear Types for Linear Algebra

Dhruv C. Makwana & Neelakantan R. Krishnaswami
We present NumLin, a functional programming language whose type system is designed to enforce the safe usage of the APIs of low-level linear algebra libraries (such as BLAS/LAPACK). We do so through a brief description of its key features and several illustrative examples. We show that NumLin's type system is sound and that its implementation improves upon naïve implementations of linear algebra programs, almost towards C-levels of performance. By doing so, we demonstrate (a) that...

Registration Year

  • 2019

Resource Types

  • Text
  • Software