Search Results

Documents authored by Haziza, Fréderic

Found 2 Possible Name Variants:

Haziza, Fréderic

Document
Invited Paper
DOI: 10.4230/OASIcs.SynCoP.2015.1
View Abstraction – A Tutorial (Invited Paper)

Authors: Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns' mutual exclusion protocol.
Cite as

Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík. View Abstraction – A Tutorial (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:OASIcs.SynCoP.2015.1,
  author =	{Abdulla, Parosh A. and Haziza, Fr\'{e}deric and Hol{\'\i}k, Luk\'{a}\v{s}},
  title =	{{View Abstraction – A Tutorial}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{1--15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.1},
  URN =		{urn:nbn:de:0030-drops-56057},
  doi =		{10.4230/OASIcs.SynCoP.2015.1},
  annote =	{Keywords: program verification, model checking, parameterized systems}
}
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.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}
}

Haziza, Frédéric

Document
Invited Paper
DOI: 10.4230/OASIcs.SynCoP.2015.1
View Abstraction – A Tutorial (Invited Paper)

Authors: Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns' mutual exclusion protocol.
Cite as

Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík. View Abstraction – A Tutorial (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:OASIcs.SynCoP.2015.1,
  author =	{Abdulla, Parosh A. and Haziza, Fr\'{e}deric and Hol{\'\i}k, Luk\'{a}\v{s}},
  title =	{{View Abstraction – A Tutorial}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{1--15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.1},
  URN =		{urn:nbn:de:0030-drops-56057},
  doi =		{10.4230/OASIcs.SynCoP.2015.1},
  annote =	{Keywords: program verification, model checking, parameterized systems}
}
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.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}
}
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