Search Results

Documents authored by Grossman, Dan

Document
DOI: 10.4230/LIPIcs.ITP.2024.33
Correctly Compiling Proofs About Programs Without Proving Compilers Correct

Authors: Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Guaranteeing correct compilation is nearly synonymous with compiler verification. However, the correctness guarantees for certified compilers and translation validation can be stronger than we need. While many compilers do have incorrect behavior, even when a compiler bug occurs it may not change the program’s behavior meaningfully with respect to its specification. Many real-world specifications are necessarily partial in that they do not completely specify all of a program’s behavior. While compiler verification and formal methods have had great success for safety-critical systems, there are magnitudes more code, such as math libraries, compiled with incorrect compilers, that would benefit from a guarantee of its partial specification. This paper explores a technique to get guarantees about compiled programs even in the presence of an unverified, or even incorrect, compiler. Our workflow compiles programs, specifications, and proof objects, from an embedded source language and logic to an embedded target language and logic. We implement two simple imperative languages, each with its own Hoare-style program logic, and a system for instantiating proof compilers out of compilers between these two languages that fulfill certain equational conditions in Coq. We instantiate our system on four compilers: one that is incomplete, two that are incorrect, and one that is correct but unverified. We use these instances to compile Hoare proofs for several programs, and we are able to leverage compiled proofs to assist in proofs of larger programs. Our proof compiler system is formally proven sound in Coq. We demonstrate how our approach enables strong target program guarantees even in the presence of incorrect compilation, opening up new options for which proof burdens one might shoulder instead of, or in addition to, compiler correctness.
Cite as

Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{seo_et_al:LIPIcs.ITP.2024.33,
  author =	{Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia},
  title =	{{Correctly Compiling Proofs About Programs Without Proving Compilers Correct}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.33},
  URN =		{urn:nbn:de:0030-drops-207612},
  doi =		{10.4230/LIPIcs.ITP.2024.33},
  annote =	{Keywords: proof transformations, compiler validation, program logics, proof engineering}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.26
Ornaments for Proof Reuse in Coq

Authors: Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
Cite as

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26,
  author =	{Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan},
  title =	{{Ornaments for Proof Reuse in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{26:1--26:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.26},
  URN =		{urn:nbn:de:0030-drops-110816},
  doi =		{10.4230/LIPIcs.ITP.2019.26},
  annote =	{Keywords: ornaments, proof reuse, proof automation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.24
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates

Authors: John Toman and Dan Grossman

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Modern software increasingly relies on external resources whose location or content can change during program execution. Examples of such resources include remote network hosts, database entries, dynamically updated configuration options, etc. Long running, adaptable programs must handle these changes gracefully and correctly. Dealing with all possible resource update scenarios is difficult to get right, especially if, as is common, external resources can be modified without prior warning by code and/or users outside of the application's direct control. If a resource unexpectedly changes during a computation, an application may observe multiple, inconsistent states of the resource, leading to incorrect program behavior. This paper presents a sound and precise static analysis, Legato, that verifies programs correctly handle changes in external resources. Our analysis ensures that every value computed by an application reflects a single, consistent version of every external resource's state. Although consistent computation in the presence of concurrent resource updates is fundamentally a concurrency issue, our analysis relies on the novel at-most-once condition to avoid explicitly reasoning about concurrency. The at-most-once condition requires that all values depend on at most one access of each resource. Our analysis is flow-, field-, and context-sensitive. It scales to real-world Java programs while producing a moderate number of false positives. We applied Legato to 10 applications with dynamically updated configurations, and found several non-trivial consistency bugs.
Cite as

John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 24:1-24:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.ECOOP.2018.24,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{24:1--24:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.24},
  URN =		{urn:nbn:de:0030-drops-92290},
  doi =		{10.4230/LIPIcs.ECOOP.2018.24},
  annote =	{Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
DOI: 10.4230/DARTS.4.3.2
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)

Authors: John Toman and Dan Grossman

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
This artifact supports Legato, an at-most-once analysis. An at-most-once analysis ensures that an application never observes inconsistent versions of its environment by checking that every value depends on at most one access of every external resource used by the application. We have applied this general analysis to the problem of finding errors in applications that support dynamic configuration updates (DCU), i.e., configuration updates that are applied immediately without program restart. When configurations may change at any point during execution, the enforcing the at-most-once condition for each configuration option guarantees that the program never observes inconsistent versions of configuration options. This artifact recreates our experiments, which applied Legato to 10 applications that support DCU and found several bugs across 9 of the 10 programs.
Cite as

John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{toman_et_al:DARTS.4.3.2,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Toman, John and Grossman, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.2},
  URN =		{urn:nbn:de:0030-drops-92342},
  doi =		{10.4230/DARTS.4.3.2},
  annote =	{Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.10
Programming Language Tools and Techniques for 3D Printing

Authors: Chandrakana Nandi, Anat Caspi, Dan Grossman, and Zachary Tatlock

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

Abstract
We propose a research agenda to investigate programming language techniques for improving affordable, end-user desktop manufacturing processes such as 3D printing. Our goal is to adapt programming languages tools and extend the decades of research in industrial, high-end CAD/CAM in order to help make affordable desktop manufacturing processes more accurate, fast, reliable, and accessible to end-users. We focus on three major areas where 3D printing can benefit from programming language tools: design synthesis, optimizing compilation, and runtime monitoring. We present preliminary results on synthesizing editable CAD models from difficult-to-edit surface meshes, discuss potential new compilation strategies, and propose runtime monitoring techniques. We conclude by discussing additional near-future directions we intend to pursue.
Cite as

Chandrakana Nandi, Anat Caspi, Dan Grossman, and Zachary Tatlock. Programming Language Tools and Techniques for 3D Printing. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 10:1-10:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{nandi_et_al:LIPIcs.SNAPL.2017.10,
  author =	{Nandi, Chandrakana and Caspi, Anat and Grossman, Dan and Tatlock, Zachary},
  title =	{{Programming Language Tools and Techniques for 3D Printing}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{10:1--10:12},
  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.10},
  URN =		{urn:nbn:de:0030-drops-71226},
  doi =		{10.4230/LIPIcs.SNAPL.2017.10},
  annote =	{Keywords: 3D printing, rapid prototyping, desktop manufacturing, compilers, verification, synthesis}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.18
Taming the Static Analysis Beast

Authors: John Toman and Dan Grossman

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

Abstract
While industrial-strength static analysis over large, real-world codebases has become commonplace, so too have difficult-to-analyze language constructs, large libraries, and popular frameworks. These features make constructing and evaluating a novel, sound analysis painful, error-prone, and tedious. We motivate the need for research to address these issues by highlighting some of the many challenges faced by static analysis developers in today's software ecosystem. We then propose our short- and long-term research agenda to make static analysis over modern software less burdensome.
Cite as

John Toman and Dan Grossman. Taming the Static Analysis Beast. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.SNAPL.2017.18,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Taming the Static Analysis Beast}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{18:1--18:14},
  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.18},
  URN =		{urn:nbn:de:0030-drops-71213},
  doi =		{10.4230/LIPIcs.SNAPL.2017.18},
  annote =	{Keywords: static analysis, frameworks, api knowledge, library specifications}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.24
Staccato: A Bug Finder for Dynamic Configuration Updates

Authors: John Toman and Dan Grossman

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Modern software applications are highly configurable, allowing configuration options to be changed even during program execution. When dynamic configuration updating is implemented incorrectly, program errors can result. These program errors occur primarily when stale data—computed from old configurations—or inconsistent data—computed from different configurations—are used. We introduce Staccato, the first tool designed to detect these errors. Staccato uses a dynamic analysis in the style of taint analysis to find the use of stale configuration data in Java programs. It supports concurrent programs running on commodity JVMs. In some cases, Staccato can provide automatic bug avoidance and semi-automatic repair when errors occur. We evaluated Staccato on 3 open-source applications that support complex reconfigurability. Staccato found multiple errors in all of them. Staccato requires only modest annotation overhead and has moderate performance overhead.
Cite as

John Toman and Dan Grossman. Staccato: A Bug Finder for Dynamic Configuration Updates. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 24:1-24:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.ECOOP.2016.24,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Staccato: A Bug Finder for Dynamic Configuration Updates}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{24:1--24:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.24},
  URN =		{urn:nbn:de:0030-drops-61185},
  doi =		{10.4230/LIPIcs.ECOOP.2016.24},
  annote =	{Keywords: Dynamic Configuration Updates, Dynamic Analysis, Software configuration}
}
Document
DOI: 10.4230/DARTS.2.1.14
Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact)

Authors: John Toman and Dan Grossman

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
This artifact is based on Staccato, a tool for finding errors in dynamic configuration update (DCU) implementations. Dynamic configuration update refers to configuration changes that occur at runtime without program restart. Errors in DCU implementations occur when stale data - computed from old configurations - or inconsistent data - computed from different configurations - are used. Staccato uses a dynamic analysis in the style of taint analysis to detect these errors. Staccato supports concurrent programs running on commodity JVMs. We evaluated Staccato on three open-source applications and found errors in all of them.
Cite as

John Toman and Dan Grossman. Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{toman_et_al:DARTS.2.1.14,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact)}},
  pages =	{14:1--14:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Toman, John and Grossman, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.14},
  URN =		{urn:nbn:de:0030-drops-61350},
  doi =		{10.4230/DARTS.2.1.14},
  annote =	{Keywords: Dynamic Configuration Updates, Dynamic Analysis, Software configuration}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.103
Toward a Dependability Case Language and Workflow for a Radiation Therapy System

Authors: Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang

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

Abstract
We present a near-future research agenda for bringing a suite of modern programming-languages verification tools - specifically interactive theorem proving, solver-aided languages, and formally defined domain-specific languages - to the development of a specific safety-critical system, a radiotherapy medical device. We sketch how we believe recent programming-languages research advances can merge with existing best practices for safety-critical systems to increase system assurance and developer productivity. We motivate hypotheses central to our agenda: That we should start with a single specific system and that we need to integrate a variety of complementary verification and synthesis tools into system development.
Cite as

Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. Toward a Dependability Case Language and Workflow for a Radiation Therapy System. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 103-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ernst_et_al:LIPIcs.SNAPL.2015.103,
  author =	{Ernst, Michael D. and Grossman, Dan and Jacky, Jon and Loncaric, Calvin and Pernsteiner, Stuart and Tatlock, Zachary and Torlak, Emina and Wang, Xi},
  title =	{{Toward a Dependability Case Language and Workflow for a Radiation Therapy System}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{103--112},
  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.103},
  URN =		{urn:nbn:de:0030-drops-50208},
  doi =		{10.4230/LIPIcs.SNAPL.2015.103},
  annote =	{Keywords: Synthesis, Proof Assistants, Verification, Dependability Cases, Domain Specific Languages, Radiation Therapy}
}
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 Imprint Privacy Contact