License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06081.6
URN: urn:nbn:de:0030-drops-7263
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/726/
Go to the corresponding Portal

Bouajjani, Ahmed ; Esparza, Javier ; Schwoon, Stefan ; Strejcek, Jan

Reachability analysis of multithreaded software with asynchronous communication

pdf-format:
06081.SchwoonStefan.Paper.726.pdf (0.2 MB)

Abstract

We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the)
thread accessing the shared memory is changed at most a fixed given
number of times. We provide efficient algorithms for both forward and
backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.

This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.

BibTeX - Entry

@InProceedings{bouajjani_et_al:DagSemProc.06081.6,
  author =	{Bouajjani, Ahmed and Esparza, Javier and Schwoon, Stefan and Strejcek, Jan},
  title =	{{Reachability analysis of multithreaded software with asynchronous communication}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/726},
  URN =		{urn:nbn:de:0030-drops-7263},
  doi =		{10.4230/DagSemProc.06081.6},
  annote =	{Keywords: Model checking, pushdown systems, concurrency}
}

Keywords: Model checking, pushdown systems, concurrency
Collection: 06081 - Software Verification: Infinite-State Model Checking and Static Program Analysis
Issue Date: 2006
Date of publication: 09.11.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI