Lock sensitive analysis of parallel programs
"Lock sensitive analysis of parallel programs" (Lock-Sensitive Analyse nebenläufiger Programme) Diese Dissertation behandelt einen Modellprüfungsalgorithmus für dynamische Pushdown-Netzwerke mit Monitoren (Monitor-DPNs). Monitor-DPNs sind ein Modell für parallele Programme mit rekursiven P...
| Author: | |
|---|---|
| Further contributors: | |
| Division/Institute: | FB 10: Mathematik und Informatik |
| Document types: | Doctoral thesis |
| Media types: | Text |
| Publication date: | 2011 |
| Date of publication on miami: | 26.07.2011 |
| Modification date: | 31.05.2016 |
| Edition statement: | [Electronic ed.] |
| Subjects: | Model-Checking; Programmanalyse; Nebenläufigkeit; Monitore; dynamische Pushdown-Netzwerke; Vorgängermengen |
| DDC Subject: | 004: Datenverarbeitung; Informatik
510: Mathematik |
| License: | InC 1.0 |
| Language: | English |
| Format: | PDF document |
| URN: | urn:nbn:de:hbz:6-43459441169 |
| Permalink: | https://nbn-resolving.de/urn:nbn:de:hbz:6-43459441169 |
| Digital documents: | diss_lammich.pdf |
"Lock sensitive analysis of parallel programs" (Lock-Sensitive Analyse nebenläufiger Programme) Diese Dissertation behandelt einen Modellprüfungsalgorithmus für dynamische Pushdown-Netzwerke mit Monitoren (Monitor-DPNs). Monitor-DPNs sind ein Modell für parallele Programme mit rekursiven Prozeduren, Thread-Erzeugung, und wechselweisem Ausschluss durch Monitore. Betrachtet werden Vorgängermengenberechnungen, mit denen man viele interessante Eigenschaften ausdrücken kann, unter Anderem Race-Conditions, Bitvektoranalysen und das (EF,EX)-Fragment der branching-time Logik CTL.