Technical Report TR-2005-06

BibliographyBouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejcek, Jan: Reachability analysis of multithreaded software with asynchronous communication.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Technical Report Computer Science No. 2005/06.
18 pages, english.
CR-SchemaD.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
Keywordssoftware verification; pushdown systems; model checking; multithreaded software
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.

Full text and
other links
PDF (187549 Bytes)
PostScript (196104 Bytes)
Contactschwoosn@fmi.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Entry dateNovember 29, 2005
   Publ. Computer Science