4 Search Results for "Poetzsch-Heffter, Arnd"


Document
09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs

Authors: Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn

Published in: Dagstuhl Seminar Proceedings, Volume 9301, Typing, Analysis and Verification of Heap-Manipulating Programs (2010)


Abstract
From July 19 to 24, 2009, the Dagstuhl Seminar 09301 ``Typing, Analysis and Verification of Heap-Manipulating Programs '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn. 09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs. In Typing, Analysis and Verification of Heap-Manipulating Programs. Dagstuhl Seminar Proceedings, Volume 9301, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{sagiv_et_al:DagSemProc.09301.1,
  author =	{Sagiv, Mooly and Poetzsch-Heffter, Arnd and O'Hearn, Peter},
  title =	{{09301 Abstracts Collection – Typing, Analysis, and Verification of Heap-Manipulating Programs}},
  booktitle =	{Typing, Analysis and Verification of Heap-Manipulating Programs},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9301},
  editor =	{Peter O'Hearn and Arnd Poetzsch-Heffter and Mooly Sagiv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09301.1},
  URN =		{urn:nbn:de:0030-drops-24361},
  doi =		{10.4230/DagSemProc.09301.1},
  annote =	{Keywords: Ownership types, static analysis, program verification, heap-manipulating programs}
}
Document
Minimal Ownership for Active Objects

Authors: David Clarke, Tobias Wrigstad, Johan Ostlund, and Einar Broch Johnsen

Published in: Dagstuhl Seminar Proceedings, Volume 9301, Typing, Analysis and Verification of Heap-Manipulating Programs (2010)


Abstract
Active objects offer a structured approach to concurrency, encapsulating both unshared state and a thread of control. For efficient data transfer, data should be passed by reference whenever possible, but this introduces aliasing and undermines the validity of the active objects. This paper proposes a minimal variant of ownership types that preserves the required race freedom invariant yet enables data transfer by reference between active objects (that is, without copying) in many cases, and a cheap clone operation where copying is necessary. Our approach is general and should be adaptable to several existing active object systems.

Cite as

David Clarke, Tobias Wrigstad, Johan Ostlund, and Einar Broch Johnsen. Minimal Ownership for Active Objects. In Typing, Analysis and Verification of Heap-Manipulating Programs. Dagstuhl Seminar Proceedings, Volume 9301, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{clarke_et_al:DagSemProc.09301.3,
  author =	{Clarke, David and Wrigstad, Tobias and Ostlund, Johan and Johnsen, Einar Broch},
  title =	{{Minimal Ownership for Active Objects}},
  booktitle =	{Typing, Analysis and Verification of Heap-Manipulating Programs},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9301},
  editor =	{Peter O'Hearn and Arnd Poetzsch-Heffter and Mooly Sagiv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09301.3},
  URN =		{urn:nbn:de:0030-drops-24379},
  doi =		{10.4230/DagSemProc.09301.3},
  annote =	{Keywords: Ownership, concurrency, uniqueness, active objects}
}
Document
09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs

Authors: Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn

Published in: Dagstuhl Seminar Proceedings, Volume 9301, Typing, Analysis and Verification of Heap-Manipulating Programs (2010)


Abstract
The document contains an executive summary of the Dagstuhl Seminar "Typing, Analysis, and Verification of Heap-Manipulating Programs" that took place July 2009.

Cite as

Mooly Sagiv, Arnd Poetzsch-Heffter, and Peter O'Hearn. 09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs. In Typing, Analysis and Verification of Heap-Manipulating Programs. Dagstuhl Seminar Proceedings, Volume 9301, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{sagiv_et_al:DagSemProc.09301.2,
  author =	{Sagiv, Mooly and Poetzsch-Heffter, Arnd and O'Hearn, Peter},
  title =	{{09301 Executive Summary – Typing, Analysis, and Verification of Heap-Manipulating Programs}},
  booktitle =	{Typing, Analysis and Verification of Heap-Manipulating Programs},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9301},
  editor =	{Peter O'Hearn and Arnd Poetzsch-Heffter and Mooly Sagiv},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09301.2},
  URN =		{urn:nbn:de:0030-drops-24354},
  doi =		{10.4230/DagSemProc.09301.2},
  annote =	{Keywords: Typing, Static Analysis, Verification, Heap-Manipulating Programs}
}
Document
Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Authors: Ina Schaefer and Arnd Poetzsch-Heffter

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
Self-adaptive embedded systems autonomously adapt to changing environment conditions to improve their functionality and to increase their dependability by downgrading functionality in case of fail- ures. However, adaptation behaviour of embedded systems significantly complicates system design and poses new challenges for guaranteeing system correctness, in particular vital in the automotive domain. Formal verification as applied in safety-critical applications must therefore be able to address not only temporal and functional properties, but also dynamic adaptation according to external and internal stimuli. In this paper, we introduce a formal semantic-based framework to model, specify and verify the functional and the adaptation behaviour of syn- chronous adaptive systems. The modelling separates functional and adap- tive behaviour to reduce the design complexity and to enable modular reasoning about both aspects independently as well as in combination. By an example, we show how to use this framework in order to verify properties of synchronous adaptive systems. Modular reasoning in com- bination with abstraction mechanisms makes automatic model checking efficiently applicable.

Cite as

Ina Schaefer and Arnd Poetzsch-Heffter. Using Abstraction in Modular Verification of Synchronous Adaptive Systems. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{schaefer_et_al:OASIcs.TrustworthySW.2006.699,
  author =	{Schaefer, Ina and Poetzsch-Heffter, Arnd},
  title =	{{Using Abstraction in Modular Verification of Synchronous Adaptive Systems}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.699},
  URN =		{urn:nbn:de:0030-drops-6996},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.699},
  annote =	{Keywords: Dependable Embedded Systems, Self-Adaptation, Abstraction, Modular Verification}
}
  • Refine by Author
  • 3 Poetzsch-Heffter, Arnd
  • 2 O'Hearn, Peter
  • 2 Sagiv, Mooly
  • 1 Clarke, David
  • 1 Johnsen, Einar Broch
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Abstraction
  • 1 Dependable Embedded Systems
  • 1 Heap-Manipulating Programs
  • 1 Modular Verification
  • 1 Ownership
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 3 2010
  • 1 2006

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