. "12"^^ . . "P(1M0545), P(GA201/03/1161), Z(MSM0021622419)" . . "RIV/00216224:14330/05:00012714" . "000234885800028" . . "Schwoon, Stefan" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication" . "[1518AC3A55E4]" . "Berlin, Heidelberg" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication"@en . "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) [QR05] and DPN (dynamic pushdown networks) [BMOT05]. 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 [QR05], 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."@en . "Esparza, Javier" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication" . "14330" . . . "2005-01-01+01:00"^^ . "Springer-Verlag" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication"@en . . . . "540074" . . "Bouajjani, Ahmed" . "3-540-30495-9" . . . . "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) [QR05] and DPN (dynamic pushdown networks) [BMOT05]. 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 [QR05], 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." . "FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference" . "bounded reachability; symbolic reachability; asynchronous dynamic pushdown network"@en . . "Hyderabad, India" . . . "4"^^ . . "Strej\u010Dek, Jan" . . "1"^^ . . "RIV/00216224:14330/05:00012714!RIV10-GA0-14330___" .