2 Search Results for "Cederberg, Jonathan"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.374
Timed Lossy Channel Systems

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
Lossy channel systems are a classical model with applications ranging from the modeling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this paper, we extend the model by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of Timed Lossy Channel Systems (TLCS). The main contribution of the paper is to show that the control state reachability problem is decidable for TLCS.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Timed Lossy Channel Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 374-386, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2012.374,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Cederberg, Jonathan},
  title =	{{Timed Lossy Channel Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{374--386},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.374},
  URN =		{urn:nbn:de:0030-drops-38746},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.374},
  annote =	{Keywords: Lossy channel systems, timed automata, model checking}
}
Document
DOI: 10.4230/DagSemProc.08171.3
Shape Analysis via Monotonic Abstraction

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

Published in: Dagstuhl Seminar Proceedings, Volume 8171, Beyond the Finite: New Challenges in Verification and Semistructured Data (2008)

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-dev.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}
}
  • Refine by Author
  • 2 Cederberg, Jonathan
  • 1 Abdulla, Parosh Aziz
  • 1 Atig, Mohamed Faouzi
  • 1 Aziz Abdulla, Parosh
  • 1 Bouajjani, Ahmed
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Lossy channel systems
  • 1 Program verification
  • 1 Shape analysis
  • 1 Static analysis
  • 1 model checking
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2008
  • 1 2012

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