Search Results

Documents authored by Bodík, Rastislav

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

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

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
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

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

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

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
Front Matter
DOI: 10.4230/LIPIcs.SNAPL.2015.i
Title, Table of Contents, Preface, List of Authors

Authors: Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morriset

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

Abstract
Title, Table of Contents, Preface, List of Authors
Cite as

1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:LIPIcs.SNAPL.2015.i,
  author =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  title =	{{Title, Table of Contents, Preface, List of Authors}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{i--xiv},
  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.i},
  URN =		{urn:nbn:de:0030-drops-50119},
  doi =		{10.4230/LIPIcs.SNAPL.2015.i},
  annote =	{Keywords: Title, Table of Contents, Preface, List of Authors}
}
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}
}
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 About DROPS Imprint Privacy Contact