10 Search Results for "Bodík, Rastislav"

Volume

LIPIcs, Volume 136

3rd Summit on Advances in Programming Languages (SNAPL 2019)

SNAPL 2019, May 16-17, 2019, Providence, RI, USA

Editors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Volume

LIPIcs, Volume 71

2nd Summit on Advances in Programming Languages (SNAPL 2017)

SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA

Editors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2019
LIPIcs, Volume 136, SNAPL'19, Complete Volume

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
LIPIcs, Volume 136, SNAPL'19, Complete Volume
Cite as

Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi. LIPIcs, Volume 136, SNAPL'19, Complete Volume. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{lerner_et_al:LIPIcs.SNAPL.2019,
  title =	{{LIPIcs, Volume 136, SNAPL'19, Complete Volume}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019},
  URN =		{urn:nbn:de:0030-drops-108657},
  doi =		{10.4230/LIPIcs.SNAPL.2019},
  annote =	{Keywords: Software and its engineering, General programming languages, Semantics}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SNAPL.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi. Front Matter, Table of Contents, Preface, Conference Organization. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 0:i-0:viii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lerner_et_al:LIPIcs.SNAPL.2019.0,
  author =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.0},
  URN =		{urn:nbn:de:0030-drops-105439},
  doi =		{10.4230/LIPIcs.SNAPL.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.10
Toward Domain-Specific Solvers for Distributed Consistency

Authors: Lindsey Kuper and Peter Alvaro

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
To guard against machine failures, modern internet services store multiple replicas of the same application data within and across data centers, which introduces the problem of keeping geo-distributed replicas consistent with one another in the face of network partitions and unpredictable message latency. To avoid costly and conservative synchronization protocols, many real-world systems provide only weak consistency guarantees (e.g., eventual, causal, or PRAM consistency), which permit certain kinds of disagreement among replicas. There has been much recent interest in language support for specifying and verifying such consistency properties. Although these properties are usually beyond the scope of what traditional type checkers or compiler analyses can guarantee, solver-aided languages are up to the task. Inspired by systems like Liquid Haskell [Vazou et al., 2014] and Rosette [Torlak and Bodik, 2014], we believe that close integration between a language and a solver is the right path to consistent-by-construction distributed applications. Unfortunately, verifying distributed consistency properties requires reasoning about transitive relations (e.g., causality or happens-before), partial orders (e.g., the lattice of replica states under a convergent merge operation), and properties relevant to message processing or API invocation (e.g., commutativity and idempotence) that cannot be easily or efficiently carried out by general-purpose SMT solvers that lack native support for this kind of reasoning. We argue that domain-specific SMT-based tools that exploit the mathematical foundations of distributed consistency would enable both more efficient verification and improved ease of use for domain experts. The principle of exploiting domain knowledge for efficiency and expressivity that has borne fruit elsewhere - such as in the development of high-performance domain-specific languages that trade off generality to gain both performance and productivity - also applies here. Languages augmented with domain-specific, consistency-aware solvers would support the rapid implementation of formally verified programming abstractions that guarantee distributed consistency. In the long run, we aim to democratize the development of such domain-specific solvers by creating a framework for domain-specific solver development that brings new theory solver implementation within the reach of programmers who are not necessarily SMT solver internals experts.
Cite as

Lindsey Kuper and Peter Alvaro. Toward Domain-Specific Solvers for Distributed Consistency. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 10:1-10:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuper_et_al:LIPIcs.SNAPL.2019.10,
  author =	{Kuper, Lindsey and Alvaro, Peter},
  title =	{{Toward Domain-Specific Solvers for Distributed Consistency}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.10},
  URN =		{urn:nbn:de:0030-drops-105530},
  doi =		{10.4230/LIPIcs.SNAPL.2019.10},
  annote =	{Keywords: distributed consistency, SMT solving, theory solvers}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2017
LIPIcs, Volume 71, SNAPL'17, Complete Volume

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
LIPIcs, Volume 71, SNAPL'17, Complete Volume
Cite as

Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi. LIPIcs, Volume 71, SNAPL'17, Complete Volume. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{lerner_et_al:LIPIcs.SNAPL.2017,
  title =	{{LIPIcs, Volume 71, SNAPL'17, Complete Volume}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017},
  URN =		{urn:nbn:de:0030-drops-71379},
  doi =		{10.4230/LIPIcs.SNAPL.2017},
  annote =	{Keywords: Programming Languages}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SNAPL.2017.0
Front Matter, Table of Contents, Preface

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
Front Matter, Table of Contents, Preface
Cite as

Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi. Front Matter, Table of Contents, Preface. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 0:i-0:viii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{lerner_et_al:LIPIcs.SNAPL.2017.0,
  author =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  title =	{{Front Matter, Table of Contents, Preface}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.0},
  URN =		{urn:nbn:de:0030-drops-71160},
  doi =		{10.4230/LIPIcs.SNAPL.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.2
Domain-Specific Symbolic Compilation

Authors: Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
A symbolic compiler translates a program to symbolic constraints, automatically reducing model checking and synthesis to constraint solving. We show that new applications of constraint solving require domain-specific encodings that yield the required orders of magnitude improvements in solver efficiency. Unfortunately, these encodings cannot be obtained with today's symbolic compilation. We introduce symbolic languages that encapsulate domain-specific encodings under abstractions that behave as their non-symbolic counterparts: client code using the abstractions can be tested and debugged on concrete inputs. When client code is symbolically compiled, the resulting constraints use domain-specific encodings. We demonstrate the idea on the first fully symbolic checker of type systems; a program partitioner; and a parallelizer of tree computations. In each of these case studies, symbolic languages improved on classical symbolic compilers by orders of magnitude.
Cite as

Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani. Domain-Specific Symbolic Compilation. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 2:1-2:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bodik_et_al:LIPIcs.SNAPL.2017.2,
  author =	{Bod{\'\i}k, Rastislav and Chandra, Kartik and Phothilimthana, Phitchaya Mangpo and Yazdani, Nathaniel},
  title =	{{Domain-Specific Symbolic Compilation}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.2},
  URN =		{urn:nbn:de:0030-drops-71334},
  doi =		{10.4230/LIPIcs.SNAPL.2017.2},
  annote =	{Keywords: Symbolic evaluation, program synthesis, DSLs}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2015
LIPIcs, Volume 32, SNAPL'15, Complete Volume

Authors: Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
LIPIcs, Volume 32, SNAPL'15, Complete Volume
Cite as

Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett. LIPIcs, Volume 32, SNAPL'15, Complete Volume. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{ball_et_al:LIPIcs.SNAPL.2015,
  title =	{{LIPIcs, Volume 32, SNAPL'15, Complete Volume}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015},
  URN =		{urn:nbn:de:0030-drops-50461},
  doi =		{10.4230/LIPIcs.SNAPL.2015},
  annote =	{Keywords: Programming Languages}
}
Document
DOI: 10.4230/DagRep.2.4.21
Software Synthesis (Dagstuhl Seminar 12152)

Authors: Rastislav Bodík, Sumit Gulwani, and Eran Yahav

Published in: Dagstuhl Reports, Volume 2, Issue 4 (2012)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12152 ``Software Synthesis''. During the seminar, several participants presented their current research, ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper. The rise of multiprocesser computers and of software verification as applied in industry combine to create an opportune moment for software synthesis. To facilitate research in this area, research from several fields of Computer Science presented tutorials on techniques they developed. This lead to (1) the definition of what challenges synthesis has to tackle in the future and (2) insights into how the several fields of synthesis are related. Finally, several groups described their experience with teaching synthesis to graduate and undergraduate students, demonstrating that synthesis is challenging for students but that they can also rise to the challenge and enjoy the field.
Cite as

Rastislav Bodík, Sumit Gulwani, and Eran Yahav. Software Synthesis (Dagstuhl Seminar 12152). In Dagstuhl Reports, Volume 2, Issue 4, pp. 21-38, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Article{bodik_et_al:DagRep.2.4.21,
  author =	{Bod{\'\i}k, Rastislav and Gulwani, Sumit and Yahav, Eran},
  title =	{{Software Synthesis (Dagstuhl Seminar 12152)}},
  pages =	{21--38},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{4},
  editor =	{Bod{\'\i}k, Rastislav and Gulwani, Sumit and Yahav, Eran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.4.21},
  URN =		{urn:nbn:de:0030-drops-35956},
  doi =		{10.4230/DagRep.2.4.21},
  annote =	{Keywords: Software Synthesis, Verification and Model Checking, Theorem Proving, Program Analysis, Programming by Demonstration, Program Derivation, Compiler Optimization}
}
  • Refine by Author
  • 6 Bodík, Rastislav
  • 5 Krishnamurthi, Shriram
  • 5 Lerner, Benjamin S.
  • 1 Alvaro, Peter
  • 1 Ball, Thomas
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → General programming languages
  • 2 Software and its engineering → Semantics
  • 1 Software and its engineering → Consistency
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Distributed computing models

  • Refine by Keyword
  • 2 Front Matter
  • 2 Preface
  • 2 Programming Languages
  • 2 Table of Contents
  • 1 Compiler Optimization
  • Show More...

  • Refine by Type
  • 8 document
  • 2 volume

  • Refine by Publication Year
  • 4 2017
  • 4 2019
  • 1 2012
  • 1 2015

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact