| Identifikační kód |
RIV/00216224:14330/05:00012714 |
| Název v anglickém jazyce |
Reachability Analysis of Multithreaded Software with Asynchronous Communication |
| Druh |
J - Recenzovaný odborný článek (Jimp, Jsc a Jost) |
| Poddruh |
- |
| Jazyk |
eng - angličtina |
| Obor - skupina |
I - Informatika |
| Obor |
IN - Informatika |
| Rok uplatnění |
2005 |
| Kód důvěrnosti údajů |
S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku |
4 |
| Počet tvůrců celkem |
4 |
| Počet domácích tvůrců |
1 |
| Výčet všech uvedených jednotlivých tvůrců |
Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915)
Ahmed Bouajjani (státní příslušnost: FR - Francouzská republika)
Javier Esparza (státní příslušnost: ES - Španělské království)
Stefan Schwoon (státní příslušnost: DE - Spolková republika Německo) |
| Popis výsledku v anglickém jazyce |
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 considersonly 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 basedon automata techniques for symbolic representation of sets of configurations. |
| Klíčová slova oddělená středníkem |
bounded reachability; symbolic reachability; asynchronous dynamic pushdown network |
| Stránka www, na které se nachází výsledek |
- |
| Odkaz na údaje z výzkumu |
- |