7 Search Results for "Toman, John"

Document
DOI: 10.4230/DagMan.10.1.1
Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)

Authors: James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter

Published in: Dagstuhl Manifestos, Volume 10, Issue 1 (2024)

Abstract
Knowledge Representation and Reasoning is a central, longstanding, and active area of Artificial Intelligence. Over the years it has evolved significantly; more recently it has been challenged and complemented by research in areas such as machine learning and reasoning under uncertainty. In July 2022,sser a Dagstuhl Perspectives workshop was held on Knowledge Representation and Reasoning. The goal of the workshop was to describe the state of the art in the field, including its relation with other areas, its shortcomings and strengths, together with recommendations for future progress. We developed this manifesto based on the presentations, panels, working groups, and discussions that took place at the Dagstuhl Workshop. It is a declaration of our views on Knowledge Representation: its origins, goals, milestones, and current foci; its relation to other disciplines, especially to Artificial Intelligence; and on its challenges, along with key priorities for the next decade.
Cite as

James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter. Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282). In Dagstuhl Manifestos, Volume 10, Issue 1, pp. 1-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{delgrande_et_al:DagMan.10.1.1,
  author =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  title =	{{Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)}},
  pages =	{1--61},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2024},
  volume =	{10},
  number =	{1},
  editor =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.10.1.1},
  URN =		{urn:nbn:de:0030-drops-201403},
  doi =		{10.4230/DagMan.10.1.1},
  annote =	{Keywords: Knowledge representation and reasoning, Applications of logics, Declarative representations, Formal logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.8
Space-Efficient Gradual Typing in Coercion-Passing Style

Authors: Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Siek et al. The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully. In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes "the rest of the run-time checks" around - just like continuation-passing style (CPS), in which "the rest of the computation" is passed around - and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from λS by Siek et al. to λS₁, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. An experimental result shows stack overflow can be prevented properly at the cost of up to 3 times slower execution for most partially typed practical programs.
Cite as

Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi. Space-Efficient Gradual Typing in Coercion-Passing Style. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tsuda_et_al:LIPIcs.ECOOP.2020.8,
  author =	{Tsuda, Yuya and Igarashi, Atsushi and Tabuchi, Tomoya},
  title =	{{Space-Efficient Gradual Typing in Coercion-Passing Style}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{8:1--8:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.8},
  URN =		{urn:nbn:de:0030-drops-131658},
  doi =		{10.4230/LIPIcs.ECOOP.2020.8},
  annote =	{Keywords: Gradual typing, coercion calculus, coercion-passing style, dynamic type checking, tail-call optimization}
}
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.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}
}
  • Refine by Author
  • 5 Grossman, Dan
  • 5 Toman, John
  • 1 Delgrande, James P.
  • 1 Glimm, Birte
  • 1 Igarashi, Atsushi
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 4 Dynamic Configuration Updates
  • 2 Dynamic Analysis
  • 2 Software configuration
  • 2 Static Analysis
  • 1 Applications of logics
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2016
  • 2 2018
  • 1 2017
  • 1 2020
  • 1 2024

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