54 Search Results for "Lal, Akash"


Volume

LIPIcs, Volume 65

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

FSTTCS 2016, December 13-15, 2016, Chennai, India

Editors: Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen

Document
Reliable State Machines: A Framework for Programming Reliable Cloud Services

Authors: Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj, Pantazis Deligiannis, Chandramouleswaran Ravichandran, Akash Lal, Aseem Rastogi, and Raja Krishnaswamy

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Building reliable applications for the cloud is challenging because of unpredictable failures during a program’s execution. This paper presents a programming framework, called Reliable State Machines (RSMs), that offers fault-tolerance by construction. In our framework, an application comprises several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is fault-tolerant by design, thereby offering the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide a .NET implementation of the RSM framework for deploying services to Microsoft Azure. We carry out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrite a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance.

Cite as

Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj, Pantazis Deligiannis, Chandramouleswaran Ravichandran, Akash Lal, Aseem Rastogi, and Raja Krishnaswamy. Reliable State Machines: A Framework for Programming Reliable Cloud Services. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{mukherjee_et_al:LIPIcs.ECOOP.2019.18,
  author =	{Mukherjee, Suvam and Raj, Nitin John and Govindraj, Krishnan and Deligiannis, Pantazis and Ravichandran, Chandramouleswaran and Lal, Akash and Rastogi, Aseem and Krishnaswamy, Raja},
  title =	{{Reliable State Machines: A Framework for Programming Reliable Cloud Services}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.18},
  URN =		{urn:nbn:de:0030-drops-108101},
  doi =		{10.4230/LIPIcs.ECOOP.2019.18},
  annote =	{Keywords: Fault tolerance, Cloud computing, Actor framework}
}
Document
Complete Volume
LIPICs, Volume 65, FSTTCS'16, Complete Volume

Authors: Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
LIPICs, Volume 65, FSTTCS'16, Complete Volume

Cite as

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Proceedings{lal_et_al:LIPIcs.FSTTCS.2016,
  title =	{{LIPICs, Volume 65, FSTTCS'16, Complete Volume}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016},
  URN =		{urn:nbn:de:0030-drops-69074},
  doi =		{10.4230/LIPIcs.FSTTCS.2016},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems Specifying and Verifying and Reasoning about Programs, Mathematical Logic, Formal Languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers

Cite as

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{lal_et_al:LIPIcs.FSTTCS.2016.0,
  author =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.0},
  URN =		{urn:nbn:de:0030-drops-68412},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
Invited Talk
Fast and Powerful Hashing Using Tabulation (Invited Talk)

Authors: Mikkel Thorup

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Randomized algorithms are often enjoyed for their simplicity, but the hash functions employed to yield the desired probabilistic guarantees are often too complicated to be practical. Here we survey recent results on how simple hashing schemes based on tabulation provide unexpectedly strong guarantees. Simple tabulation hashing dates back to Zobrist [1970]. Keys are viewed as consisting of c characters and we have precomputed character tables h_1, ... , h_q mapping characters to random hash values. A key x = (x_1 , ..., x_c) is hashed to h_1[x_1] + h_2[x_2] ... + h_c[x_c]. This scheme is very fast with character tables in cache. While simple tabulation is not even 4-independent, it does provide many of the guarantees that are normally obtained via higher independence, e.g., linear probing and Cuckoo hashing. Next we consider twisted tabulation where one character is "twisted" with some simple operations. The resulting hash function has powerful distributional properties: Chernoff-Hoeffding type tail bounds and a very small bias for min-wise hashing. Finally, we consider double tabulation where we compose two simple tabulation functions, applying one to the output of the other, and show that this yields very high independence in the classic framework of Carter and Wegman [1977]. In fact, w.h.p., for a given set of size proportional to that of the space consumed, double tabulation gives fully-random hashing. While these tabulation schemes are all easy to implement and use, their analysis is not.

Cite as

Mikkel Thorup. Fast and Powerful Hashing Using Tabulation (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{thorup:LIPIcs.FSTTCS.2016.1,
  author =	{Thorup, Mikkel},
  title =	{{Fast and Powerful Hashing Using Tabulation}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.1},
  URN =		{urn:nbn:de:0030-drops-68869},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.1},
  annote =	{Keywords: Hashing, Randomized Algorithms}
}
Document
Invited Talk
Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk)

Authors: Mooly Sagiv

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants—an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver. This is a joint work with Ken McMillan (Microsoft Research), Oded Padon (Tel Aviv University), Aurojit Panda (UC Berkeley), and Sharon Shoham (Tel Aviv University) and was integrated into the IVY system. The work is inspired by Shachar Itzhaky's thesis.

Cite as

Mooly Sagiv. Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{sagiv:LIPIcs.FSTTCS.2016.2,
  author =	{Sagiv, Mooly},
  title =	{{Simple Invariants for Proving the Safety of Distributed Protocols}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.2},
  URN =		{urn:nbn:de:0030-drops-68877},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.2},
  annote =	{Keywords: Program verification, Distributed protocols, Deductive reasoning}
}
Document
Invited Talk
My O Is Bigger Than Yours (Invited Talk)

Authors: Holger Hermanns

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
This invited talk starts off with a review of probabilistic safety assessment (PSA) methods currently exercised across the nuclear power plant domain worldwide. It then elaborates on crucial aspects of the Fukushima Dai-ichi accident which are not considered properly in contemporary PSA studies. New kinds of PSA are needed so as to take into account external hazards, dynamic aspects of accident progression, and partial information. All of these come with obvious increases in algorithmic analysis complexity. This motivates our ongoing work to gradually tackle the resulting modelling and analysis problems. They revolve around static and dynamic fault trees, open interpretations of compositional Markov models and advances in their effective numerical analysis.

Cite as

Holger Hermanns. My O Is Bigger Than Yours (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{hermanns:LIPIcs.FSTTCS.2016.3,
  author =	{Hermanns, Holger},
  title =	{{My O Is Bigger Than Yours}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.3},
  URN =		{urn:nbn:de:0030-drops-68881},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.3},
  annote =	{Keywords: Probabilistic Safety Analysis, Fault Trees, Compositionality, Markov Models, Model Checking}
}
Document
Invited Talk
Continuous Optimization: The “Right” Language for Graph Algorithms? (Invited Talk)

Authors: Aleksander Madry

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Traditionally, we view graphs as purely combinatorial objects and tend to design our graph algorithms to be combinatorial as well. In fact, in the context of algorithms, "combinatorial" became a synonym of "fast". Recent work, however, shows that a number of such "inherently combinatorial" graph problems can be solved much faster using methods that are very "non-combinatorial". Specifically, by approaching these problems with tools and notions borrowed from linear algebra and, more broadly, from continuous optimization. A notable examples here are the recent lines of work on the maximum flow problem, the bipartite matching problem, and the shortest path problem in graphs with negative-length arcs. This raises an intriguing question: Is continuous optimization a more suitable and principled optics for fast graph algorithms than the classic combinatorial view? In this talk, I will discuss this question as well as the developments that motivated it.

Cite as

Aleksander Madry. Continuous Optimization: The “Right” Language for Graph Algorithms? (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{madry:LIPIcs.FSTTCS.2016.4,
  author =	{Madry, Aleksander},
  title =	{{Continuous Optimization: The “Right” Language for Graph Algorithms?}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.4},
  URN =		{urn:nbn:de:0030-drops-68890},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.4},
  annote =	{Keywords: maximum flow problem, bipartite matchings, interior-point methods, gradient decent method, Laplacian linear systems}
}
Document
Invited Talk
Graph Decompositions and Algorithms (Invited Talk)

Authors: Fedor V. Fomin

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
We overview the recent progress in solving intractable optimization problems on planar graphs as well as other classes of sparse graphs. In particular, we discuss how tools from Graph Minors theory can be used to obtain: * subexponential parameterized algorithms * approximation algorithms, and * preprocessing and kernelization algorithms on these classes of graphs.

Cite as

Fedor V. Fomin. Graph Decompositions and Algorithms (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{fomin:LIPIcs.FSTTCS.2016.5,
  author =	{Fomin, Fedor V.},
  title =	{{Graph Decompositions and Algorithms}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.5},
  URN =		{urn:nbn:de:0030-drops-68903},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.5},
  annote =	{Keywords: Algorithms, logic, graph minor}
}
Document
Invited Talk
Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk)

Authors: Tevfik Bultan

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
A crucial problem in software security is the detection of side-channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). In this talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. In addition to computing information leakage for a single run of a program, I will also discuss computation of information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. For segmented oracles, it is possible to compute information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. These results have been implemented as an extension to the symbolic execution tool Symbolic Path Finder (SPF) using the SMT solver Z3 and two model counting constraint solvers LattE and ABC.

Cite as

Tevfik Bultan. Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bultan:LIPIcs.FSTTCS.2016.6,
  author =	{Bultan, Tevfik},
  title =	{{Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{6:1--6:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.6},
  URN =		{urn:nbn:de:0030-drops-68914},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.6},
  annote =	{Keywords: Side-channels, quantitative information flow, symbolic execution, model counting, constraint solvers}
}
Document
Mixed-Criticality Scheduling to Minimize Makespan

Authors: Sanjoy Baruah, Arvind Easwaran, and Zhishan Guo

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
In the mixed-criticality job model, each job is characterized by two execution time parameters, representing a smaller (less conservative) estimate and a larger (more conservative) estimate on its actual, unknown, execution time. Each job is further classified as being either less critical or more critical. The desired execution semantics are that all jobs should execute correctly provided all jobs complete upon being allowed to execute for up to the smaller of their execution time estimates, whereas if some jobs need to execute beyond their smaller execution time estimates (but not beyond their larger execution time estimates), then only the jobs classified as being more critical are required to execute correctly. The scheduling of collections of such mixed-criticality jobs upon identical multiprocessor platforms in order to minimize the makespan is considered here.

Cite as

Sanjoy Baruah, Arvind Easwaran, and Zhishan Guo. Mixed-Criticality Scheduling to Minimize Makespan. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{baruah_et_al:LIPIcs.FSTTCS.2016.7,
  author =	{Baruah, Sanjoy and Easwaran, Arvind and Guo, Zhishan},
  title =	{{Mixed-Criticality Scheduling to Minimize Makespan}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{7:1--7:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.7},
  URN =		{urn:nbn:de:0030-drops-68429},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.7},
  annote =	{Keywords: Scheduling, Mixed criticality, Identical parallel machines, Makespan minimization, Approximation algorithm.}
}
Document
Capacitated k-Center Problem with Vertex Weights

Authors: Aounon Kumar

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
We study the capacitated k-center problem with vertex weights. It is a generalization of the well known k-center problem. In this variant each vertex has a weight and a capacity. The assignment cost of a vertex to a center is given by the product of the weight of the vertex and its distance to the center. The distances are assumed to form a metric. Each center can only serve as many vertices as its capacity. We show an n^{1-epsilon}-approximation hardness for this problem, for any epsilon > 0, where n is the number of vertices in the input. Both the capacitated and the weighted versions of the k-center problem individually can be approximated within a constant factor. Yet the common extension of both the generalizations cannot be approximated efficiently within a constant factor, unless P = NP. This problem, to the best of our knowledge, is the first facility location problem with metric distances known to have a super-constant inapproximability result. The hardness result easily generalizes to versions of the problem that consider the p-norm of the assignment costs (weighted distances) as the objective function. We give n^{1- 1/p - epsilon}-approximation hardness for this problem, for p>1. We complement the hardness result by showing a simple n-approximation algorithm for this problem. We also give a bi-criteria constant factor approximation algorithm, for the case of uniform capacities, which opens at most 2k centers.

Cite as

Aounon Kumar. Capacitated k-Center Problem with Vertex Weights. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kumar:LIPIcs.FSTTCS.2016.8,
  author =	{Kumar, Aounon},
  title =	{{Capacitated k-Center Problem with Vertex Weights}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{8:1--8:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.8},
  URN =		{urn:nbn:de:0030-drops-68438},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.8},
  annote =	{Keywords: approximation hardness, k-center, gadget reduction}
}
Document
Improved Pseudo-Polynomial-Time Approximation for Strip Packing

Authors: Waldo Gálvez, Fabrizio Grandoni, Salvatore Ingala, and Arindam Khan

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
We study the strip packing problem, a classical packing problem which generalizes both bin packing and makespan minimization. Here we are given a set of axis-parallel rectangles in the two-dimensional plane and the goal is to pack them in a vertical strip of fixed width such that the height of the obtained packing is minimized. The packing must be non-overlapping and the rectangles cannot be rotated. A reduction from the partition problem shows that no approximation better than 3/2 is possible for strip packing in polynomial time (assuming P!=NP). Nadiradze and Wiese [SODA16] overcame this barrier by presenting a (7/5+epsilon)-approximation algorithm in pseudo-polynomial-time (PPT). As the problem is strongly NP-hard, it does not admit an exact PPT algorithm (though a PPT approximation scheme might exist). In this paper we make further progress on the PPT approximability of strip packing, by presenting a (4/3+epsilon)-approximation algorithm. Our result is based on a non-trivial repacking of some rectangles in the "empty space" left by the construction by Nadiradze and Wiese, and in some sense pushes their approach to its limit. Our PPT algorithm can be adapted to the case where we are allowed to rotate the rectangles by 90 degrees, achieving the same approximation factor and breaking the polynomial-time approximation barrier of 3/2 for the case with rotations as well.

Cite as

Waldo Gálvez, Fabrizio Grandoni, Salvatore Ingala, and Arindam Khan. Improved Pseudo-Polynomial-Time Approximation for Strip Packing. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{galvez_et_al:LIPIcs.FSTTCS.2016.9,
  author =	{G\'{a}lvez, Waldo and Grandoni, Fabrizio and Ingala, Salvatore and Khan, Arindam},
  title =	{{Improved Pseudo-Polynomial-Time Approximation for Strip Packing}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.9},
  URN =		{urn:nbn:de:0030-drops-68445},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.9},
  annote =	{Keywords: approximation algorithms, strip packing, rectangle packing, cutting-stock problem}
}
Document
Embedding Approximately Low-Dimensional l_2^2 Metrics into l_1

Authors: Amit Deshpande, Prahladh Harsha, and Rakesh Venkat

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Goemans showed that any n points x_1,..., x_n in d-dimensions satisfying l_2^2 triangle inequalities can be embedded into l_{1}, with worst-case distortion at most sqrt{d}. We consider an extension of this theorem to the case when the points are approximately low-dimensional as opposed to exactly low-dimensional, and prove the following analogous theorem, albeit with average distortion guarantees: There exists an l_{2}^{2}-to-l_{1} embedding with average distortion at most the stable rank, sr(M), of the matrix M consisting of columns {x_i-x_j}_{i<j}. Average distortion embedding suffices for applications such as the SPARSEST CUT problem. Our embedding gives an approximation algorithm for the SPARSEST CUT problem on low threshold-rank graphs, where earlier work was inspired by Lasserre SDP hierarchy, and improves on a previous result of the first and third author [Deshpande and Venkat, in Proc. 17th APPROX, 2014]. Our ideas give a new perspective on l_{2}^{2} metric, an alternate proof of Goemans' theorem, and a simpler proof for average distortion sqrt{d}.

Cite as

Amit Deshpande, Prahladh Harsha, and Rakesh Venkat. Embedding Approximately Low-Dimensional l_2^2 Metrics into l_1. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{deshpande_et_al:LIPIcs.FSTTCS.2016.10,
  author =	{Deshpande, Amit and Harsha, Prahladh and Venkat, Rakesh},
  title =	{{Embedding Approximately Low-Dimensional l\underline2^2 Metrics into l\underline1}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{10:1--10:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.10},
  URN =		{urn:nbn:de:0030-drops-68456},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.10},
  annote =	{Keywords: Metric Embeddings, Sparsest Cut, Negative type metrics, Approximation Algorithms}
}
Document
Relational Logic with Framing and Hypotheses

Authors: Anindya Banerjee, David A. Naumann, and Mohammad Nikouei

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.

Cite as

Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{banerjee_et_al:LIPIcs.FSTTCS.2016.11,
  author =	{Banerjee, Anindya and Naumann, David A. and Nikouei, Mohammad},
  title =	{{Relational Logic with Framing and Hypotheses}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.11},
  URN =		{urn:nbn:de:0030-drops-68465},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.11},
  annote =	{Keywords: Relational Hoare logic, program equivalence, product programs, frame conditions, region logic}
}
  • Refine by Author
  • 3 Lal, Akash
  • 2 Akshay, S.
  • 2 Harsha, Prahladh
  • 2 Krishna, Shankara Narayanan
  • 2 Panolan, Fahad
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Cloud computing
  • 1 Software and its engineering → Software fault tolerance
  • 1 Software and its engineering → Software reliability

  • Refine by Keyword
  • 3 Model Checking
  • 2 Algorithms
  • 2 Infinite Games
  • 2 Online Algorithms
  • 2 approximation algorithms
  • Show More...

  • Refine by Type
  • 53 document
  • 1 volume

  • Refine by Publication Year
  • 53 2016
  • 1 2019

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