732 Works

Extended Formulation Lower Bounds via Hypergraph Coloring?

Stavros G. Kolliopoulos & Yannis Moysoglou
Exploring the power of linear programming for combinatorial optimization problems has been recently receiving renewed attention after a series of breakthrough impossibility results. From an algorithmic perspective, the related questions concern whether there are compact formulations even for problems that are known to admit polynomial-time algorithms. We propose a framework for proving lower bounds on the size of extended formulations. We do so by introducing a specific type of extended relaxations that we call product...

Approximating Hit Rate Curves using Streaming Algorithms

Zachary Drudi, Nicholas J. A. Harvey, Stephen Ingram, Andrew Warfield & Jake Wires
A hit rate curve is a function that maps cache size to the proportion of requests that can be served from the cache. (The caching policy and sequence of requests are assumed to be fixed.) Hit rate curves have been studied for decades in the operating system, database and computer architecture communities. They are useful tools for designing appropriate cache sizes, dynamically allocating memory between competing caches, and for summarizing locality properties of the request...

Multivariate Amortised Resource Analysis for Term Rewrite Systems

Martin Hofmann & Georg Moser
We study amortised resource analysis in the context of term rewrite systems. We introduce a novel amortised analysis based on the potential method. The method is represented in an inference system akin to a type system and gives rise to polynomial bounds on the innermost runtime complexity of the analysed rewrite system. The crucial feature of the inference system is the admittance of multivariate bounds in the context of arbitrary data structures in a completely...

Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems

Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel & Kunle Olukotun
Most performance critical software is developed using very low-level techniques. We argue that this needs to change, and that generative programming is an effective avenue to enable the use of high-level languages and programming techniques in many such circumstances.

Toward Automatic Verification of Quantum Cryptographic Protocols

Yuan Feng & Mingsheng Ying
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to...

Comparing 1D and 2D Real Time on Cellular Automata

Anaël Grandjean & Victor Poupet
We study the influence of the dimension of cellular automata (CA) for real time language recognition of one-dimensional languages with parallel input. Specifically, we focus on the question of determining whether every language that can be recognized in real time on a 2-dimensional CA working on the Moore neighborhood can also be recognized in real time by a 1-dimensional CA working on the standard two-way neighborhood. We show that 2-dimensional CA in real time can...

Inferring Lower Bounds for Runtime Complexity

Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann & Thomas Ströder
We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term...

Modeling Real-World Data Sets (Invited Talk)

Susanne Albers
Traditionally, the performance of algorithms is evaluated using worst-case analysis. For a number of problems, this type of analysis gives overly pessimistic results: Worst-case inputs are rather artificial and do not occur in practical applications. In this lecture we review some alternative analysis approaches leading to more realistic and robust performance evaluations. Specifically, we focus on the approach of modeling real-world data sets. We report on two studies performed by the author for the problems...

From Episodic Memory to Narrative in a Cognitive Architecture

Tory S. Anderson

Modal Logics for Nominal Transition Systems

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas & Tjark Weber
We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The...

Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis

Alvin Cheung, Shoaib Kamil & Armando Solar-Lezama
This paper describes a new approach to program optimization that allows general purpose code to benefit from the optimization power of domain-specific compilers. The key to this approach is a synthesis-based technique to raise the level of abstraction of general-purpose code to enable aggressive domain-specific optimizations. We have been implementing this approach in an extensible system called Herd. The system is designed around a collection of parameterized kernel translators. Each kernel translator is associated with...

Mixin Composition Synthesis Based on Intersection Types

Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo De’Liguoro & Jakob Rehof
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and record-merge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with...

Globalizing Domain-Specific Languages (Dagstuhl Seminar 14412)

Betty H. C. Cheng, Benoit Combemale, Robert B. France, Jean-Marc Jézéquel & Bernhard Rumpe
This report documents the program and the outcomes of the Dagstuhl Seminar 14412 "Globalizing Domain-Specific Languages" held in October 2014. Complex, data-intensive, cyper-physical, cloud-based etc. systems need effective modeling techniques, preferably based on DSLs to describe aspects and views. Models written in heterogeneous languages however need to be semantically compatible and their supporting individual tools need to be interoperable. This workshop discusses possible and necessary forms of interoperation their benefits and drawbacks and in particular...

Parameterized Lower Bound and Improved Kernel for Diamond-free Edge Deletion

R. B. Sandeep & Naveen Sivadasan
A diamond is a graph obtained by removing an edge from a complete graph on four vertices. A graph is diamond-free if it does not contain an induced diamond. The Diamond-free Edge Deletion problem asks to find whether there exist at most k edges in the input graph whose deletion results in a diamond-free graph. The problem was proved to be NP-complete and a polynomial kernel of O(k^4) vertices was found by Fellows et. al....

Average Distance Queries through Weighted Samples in Graphs and Metric Spaces: High Scalability with Tight Statistical Guarantees

Shiri Chechik, Edith Cohen & Haim Kaplan
The average distance from a node to all other nodes in a graph, or from a query point in a metric space to a set of points, is a fundamental quantity in data analysis. The inverse of the average distance, known as the (classic) closeness centrality of a node, is a popular importance measure in the study of social networks. We develop novel structural insights on the sparsifiability of the distance relation via weighted sampling....

Parameter Compilation

Hubie Chen

Front Matter, Table of Contents, Preface, Conference Organization

Lars Arge & János Pach
Front Matter, Table of Contents, Preface, Conference Organization

The Container Selection Problem

Viswanath Nagarajan, Kanthi K. Sarpatwar, Baruch Schieber, Hadas Shachnai & Joel L. Wolf
We introduce and study a network resource management problem that is a special case of non-metric k-median, naturally arising in cross platform scheduling and cloud computing. In the continuous d-dimensional container selection problem, we are given a set C of input points in d-dimensional Euclidean space, for some d >= 2, and a budget k. An input point p can be assigned to a "container point" c only if c dominates p in every dimension....

Parameterized Complexity of Graph Constraint Logic

Tom C. Van Der Zanden
Graph constraint logic is a framework introduced by Hearn and Demaine, which provides several problems that are often a convenient starting point for reductions. We study the parameterized complexity of Constraint Graph Satisfiability and both bounded and unbounded versions of Nondeterministic Constraint Logic (NCL) with respect to solution length, treewidth and maximum degree of the underlying constraint graph as parameters. As a main result we show that restricted NCL remains PSPACE-complete on graphs of bounded...

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

Mladen Miksa & Jakob Nordström
We study the problem of establishing lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can...

On Constant-Size Graphs That Preserve the Local Structure of High-Girth Graphs

Hendrik Fichtenberger, Pan Peng & Christian Sohler
Let G=(V,E) be an undirected graph with maximum degree d. The k-disc of a vertex v is defined as the rooted subgraph that is induced by all vertices whose distance to v is at most k. The k-disc frequency vector of G, freq(G), is a vector indexed by all isomorphism types of k-discs. For each such isomorphism type Gamma, the k-disc frequency vector counts the fraction of vertices that have k-disc isomorphic to Gamma. Thus,...

On the Workflow Satisfiability Problem with Class-independent Constraints

Jason Crampton, Andrei Gagarin, Gregory Gutin & Mark Jones
A workflow specification defines sets of steps and users. An authorization policy determines for each user a subset of steps the user is allowed to perform. Other security requirements, such as separation-of-duty, impose constraints on which subsets of users may perform certain subsets of steps. The workflow satisfiability problem (WSP) is the problem of determining whether there exists an assignment of users to workflow steps that satisfies all such authorizations and constraints. An algorithm for...

Coalgebraic Infinite Traces and Kleisli Simulations

Natsuke Urabe & Ichiro Hasuo
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors. In...

Final Coalgebras from Corecursive Algebras

Paul Blain Levy

Sparsification Upper and Lower Bounds for Graphs Problems and Not-All-Equal SAT

Bart M. P. Jansen & Astrid Pieterse

Registration Year

  • 2015

Resource Types

  • Text
  • Software