"DE - Spolkov\u00E1 republika N\u011Bmecko" . . "1"^^ . . "3821" . . "bounded reachability; symbolic reachability; asynchronous dynamic pushdown network"@en . "Lecture Notes in Computer Science" . "Anal\u00FDza dosa\u017Eitelnosti pro v\u00EDcevl\u00E1knov\u00E9 programy s asynchronn\u00ED komunikac\u00ED"@cs . "P\u0159edstavujeme Asynchronni dynamick\u00E9 z\u00E1sobn\u00EDkov\u00E9 s\u00EDt\u011B (ADPN) jako nov\u00FD model pro v\u00EDcevl\u00E1knov\u00E9 programy, ve kter\u00E9m z\u00E1sobn\u00EDkov\u00E9 syst\u00E9my komunikuj\u00ED p\u0159es sd\u00EDlenou pam\u011B\u0165. ADPN zobec\u0148uje CPS (soub\u011B\u017En\u00E9 z\u00E1sobn\u00EDkov\u00E9 syst\u00E9my) [QR05] a DPN (dynamick\u00E9 z\u00E1sobn\u00EDkov\u00E9 s\u00EDt\u011B) [BMOT05]. Uk\u00E1\u017Eeme, \u017Ee ADPN maj\u00ED n\u011Bkolik v\u00FDhod. Jeliko\u017E probl\u00E9m dosa\u017Eitelnosti pro ADPN je nerozhodnuteln\u00FD i pro p\u0159\u00EDpad bez dynamick\u00E9ho vytv\u00E1\u0159en\u00ED proces\u016F, zab\u00FDv\u00E1me se probl\u00E9mem omezen\u00E9 dosa\u017Eitelnosti [QR05], kter\u00FD uva\u017Euje jenom ty v\u00FDpo\u010Detn\u00ED b\u011Bhy, kde po\u010Det zm\u011Bn (indexu) procesu momet\u00E1ln\u011B p\u0159istupuj\u00EDc\u00EDmu ke sd\u00EDlen\u00E9 pam\u011Bti omezen dan\u00FDm \u010D\u00EDslem. Poskytujeme efektivn\u00ED algoritmy pro anal\u00FDzu dop\u0159edn\u00E9 i zp\u011Btn\u00E9 dosa\u017Eitelnosti. Tyto algoritmy vyu\u017E\u00EDvaj\u00ED zn\u00E1m\u00E9 techniky pracuj\u00EDc\u00ED s automaty, kter\u00E9 reprezentuj\u00ED mno\u017Einy konfigurac\u00ED."@cs . . . . "4"^^ . "P(1M0545), P(GA201/03/1161), Z(MSM0021622419)" . "Anal\u00FDza dosa\u017Eitelnosti pro v\u00EDcevl\u00E1knov\u00E9 programy s asynchronn\u00ED komunikac\u00ED"@cs . "RIV/00216224:14330/05:00012714" . "RIV/00216224:14330/05:00012714!RIV08-MSM-14330___" . "Schwoon, Stefan" . . . . "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 . . . "Reachability Analysis of Multithreaded Software with Asynchronous Communication"@en . "Bouajjani, Ahmed" . . . "[0BAE9F484B0B]" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication"@en . . "2005" . "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." . . . . "Esparza, Javier" . "540075" . "348-359" . "14330" . "Reachability Analysis of Multithreaded Software with Asynchronous Communication" . . "12"^^ . "Reachability Analysis of Multithreaded Software with Asynchronous Communication" . "0302-9743" . "Strej\u010Dek, Jan" .