Volume

Dagstuhl Seminar Proceedings, Volume 8171



Publication Details

  • published at: 2008-07-23
  • Publisher: Schloss-Dagstuhl - Leibniz Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
08171 Abstracts Collection – Beyond the Finite: New Challenges in Verification and Semistructured Data

Authors: Anca Muscholl, Ramaswamy Ramanujam, Michaël Rusinowitch, Thomas Schwentick, and Victor Vianu


Abstract
From 20.04. to 25.04.2008, the Dagstuhl Seminar 08171 ``Beyond the Finite: New Challenges in Verification and Semistructured Data'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. 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

Anca Muscholl, Ramaswamy Ramanujam, Michaël Rusinowitch, Thomas Schwentick, and Victor Vianu. 08171 Abstracts Collection – Beyond the Finite: New Challenges in Verification and Semistructured Data. In Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, Volume 8171, pp. 1-14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{muscholl_et_al:DagSemProc.08171.1,
  author =	{Muscholl, Anca and Ramanujam, Ramaswamy and Rusinowitch, Micha\"{e}l and Schwentick, Thomas and Vianu, Victor},
  title =	{{08171 Abstracts Collection – Beyond the Finite: New Challenges in Verification and Semistructured Data}},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8171},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha\"{e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08171.1},
  URN =		{urn:nbn:de:0030-drops-15606},
  doi =		{10.4230/DagSemProc.08171.1},
  annote =	{Keywords: Infinite state systems, data values, verification, semistructured data}
}
Document
08171 Summary – Beyond the Finite: New Challenges in Verification and Semistructured Data

Authors: Anca Muscholl, Ramaswamy Ramanujam, Michaël Rusinowitch, Thomas Schwentick, and Victor Vianu


Abstract
Exploring the interaction of model checking and database static analysis techniques in the development of novel approaches to the verification of software systems handling data.

Cite as

Anca Muscholl, Ramaswamy Ramanujam, Michaël Rusinowitch, Thomas Schwentick, and Victor Vianu. 08171 Summary – Beyond the Finite: New Challenges in Verification and Semistructured Data. In Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, Volume 8171, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{muscholl_et_al:DagSemProc.08171.2,
  author =	{Muscholl, Anca and Ramanujam, Ramaswamy and Rusinowitch, Micha\"{e}l and Schwentick, Thomas and Vianu, Victor},
  title =	{{08171 Summary – Beyond the Finite: New Challenges in Verification and Semistructured Data}},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8171},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha\"{e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08171.2},
  URN =		{urn:nbn:de:0030-drops-15580},
  doi =		{10.4230/DagSemProc.08171.2},
  annote =	{Keywords: Infinite state systems, data values, verification, semistructured data}
}
Document
Shape Analysis via Monotonic Abstraction

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, and Ahmed Rezine


Abstract
We propose a new formalism for reasoning about dynamic memory heaps, using monotonic abstraction and symbolic backward reachability analysis. We represent the heaps as graphs, and introduce an ordering on these graphs. This enables us to represent the violation of a given safety property as the reachability of a finitely representable set of bad graphs. We also describe how to symbolically compute the reachable states in the transition system induced by a program.

Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, and Ahmed Rezine. Shape Analysis via Monotonic Abstraction. In Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, Volume 8171, pp. 1-11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{azizabdulla_et_al:DagSemProc.08171.3,
  author =	{Aziz Abdulla, Parosh and Bouajjani, Ahmed and Cederberg, Jonathan and Haziza, Fr\'{e}d\'{e}ric and Ji, Ran and Rezine, Ahmed},
  title =	{{Shape Analysis via Monotonic Abstraction}},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8171},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha\"{e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08171.3},
  URN =		{urn:nbn:de:0030-drops-15590},
  doi =		{10.4230/DagSemProc.08171.3},
  annote =	{Keywords: Shape analysis, Program verification, Static analysis}
}

Filters


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