5 Search Results for "Ernst, Michael D."

Document
Artifact
DOI: 10.4230/DARTS.8.2.22
Accumulation Analysis (Artifact)

Authors: Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This artifact contains the data and analysis supporting the literature survey in section 4 of [Kellogg et al., 2022]. In our literature survey, we examined 187 papers from the literature that mention "typestate" and analyzed the typestate specifications they contained to determine whether or not they are accumulation typestate specifications. Our purpose in doing this literature survey was to determine whether typestate FSMs were accumulation or not. However, we believe that the collection of typestate automata in typestates.pdf might be useful to anyone interested in the sort of typestate automata that appear in the literature. If we had had access to such a collection (gathered for a different purpose), our classification of whether these typestate automata were accumulation would have been much simpler. Anyone interested in properties of typestate automata can re-use our work.
Cite as

Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation Analysis (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kellogg_et_al:DARTS.8.2.22,
  author =	{Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
  title =	{{Accumulation Analysis (Artifact)}},
  pages =	{22:1--22:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.22},
  URN =		{urn:nbn:de:0030-drops-162209},
  doi =		{10.4230/DARTS.8.2.22},
  annote =	{Keywords: Typestate, finite-state property}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.10
Accumulation Analysis

Authors: Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
A typestate specification indicates which behaviors of an object are permitted in each of the object’s states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.
Cite as

Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation Analysis. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kellogg_et_al:LIPIcs.ECOOP.2022.10,
  author =	{Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
  title =	{{Accumulation Analysis}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{10:1--10:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.10},
  URN =		{urn:nbn:de:0030-drops-162381},
  doi =		{10.4230/LIPIcs.ECOOP.2022.10},
  annote =	{Keywords: Typestate, finite-state property}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.4
Natural Language is a Programming Language: Applying Natural Language Processing to Software Development

Authors: Michael D. Ernst

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

Abstract
A powerful, but limited, way to view software is as source code alone. Treating a program as a sequence of instructions enables it to be formalized and makes it amenable to mathematical techniques such as abstract interpretation and model checking. A program consists of much more than a sequence of instructions. Developers make use of test cases, documentation, variable names, program structure, the version control repository, and more. I argue that it is time to take the blinders off of software analysis tools: tools should use all these artifacts to deduce more powerful and useful information about the program. Researchers are beginning to make progress towards this vision. This paper gives, as examples, four results that find bugs and generate code by applying natural language processing techniques to software artifacts. The four techniques use as input error messages, variable names, procedure documentation, and user questions. They use four different NLP techniques: document similarity, word semantics, parse trees, and neural networks. The initial results suggest that this is a promising avenue for future work.
Cite as

Michael D. Ernst. Natural Language is a Programming Language: Applying Natural Language Processing to Software Development. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 4:1-4:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ernst:LIPIcs.SNAPL.2017.4,
  author =	{Ernst, Michael D.},
  title =	{{Natural Language is a Programming Language: Applying Natural Language Processing to Software Development}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{4:1--4: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.4},
  URN =		{urn:nbn:de:0030-drops-71357},
  doi =		{10.4230/LIPIcs.SNAPL.2017.4},
  annote =	{Keywords: natural language processing, program analysis, software development}
}
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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.197
Arc Diagrams, Flip Distances, and Hamiltonian Triangulations

Authors: Jean Cardinal, Michael Hoffmann, Vincent Kusters, Csaba D. Tóth, and Manuel Wettstein

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
We show that every triangulation (maximal planar graph) on n\ge 6 vertices can be flipped into a Hamiltonian triangulation using a sequence of less than n/2 combinatorial edge flips. The previously best upper bound uses 4-connectivity as a means to establish Hamiltonicity. But in general about 3n/5 flips are necessary to reach a 4-connected triangulation. Our result improves the upper bound on the diameter of the flip graph of combinatorial triangulations on n vertices from 5.2n-33.6 to 5n-23. We also show that for every triangulation on n vertices there is a simultaneous flip of less than 2n/3 edges to a 4-connected triangulation. The bound on the number of edges is tight, up to an additive constant. As another application we show that every planar graph on n vertices admits an arc diagram with less than n/2 biarcs, that is, after subdividing less than n/2 (of potentially 3n-6) edges the resulting graph admits a 2-page book embedding.
Cite as

Jean Cardinal, Michael Hoffmann, Vincent Kusters, Csaba D. Tóth, and Manuel Wettstein. Arc Diagrams, Flip Distances, and Hamiltonian Triangulations. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 197-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cardinal_et_al:LIPIcs.STACS.2015.197,
  author =	{Cardinal, Jean and Hoffmann, Michael and Kusters, Vincent and T\'{o}th, Csaba D. and Wettstein, Manuel},
  title =	{{Arc Diagrams, Flip Distances, and Hamiltonian Triangulations}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{197--210},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.197},
  URN =		{urn:nbn:de:0030-drops-49141},
  doi =		{10.4230/LIPIcs.STACS.2015.197},
  annote =	{Keywords: graph embeddings, edge flips, flip graph, separating triangles}
}
  • Refine by Author
  • 4 Ernst, Michael D.
  • 2 Kellogg, Martin
  • 2 Shadab, Narges
  • 2 Sridharan, Manu
  • 1 Cardinal, Jean
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Formal software verification

  • Refine by Keyword
  • 2 Typestate
  • 2 finite-state property
  • 1 Dependability Cases
  • 1 Domain Specific Languages
  • 1 Proof Assistants
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2015
  • 2 2022
  • 1 2017

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