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...
| Verfasser: | |
|---|---|
| Weitere Beteiligte: | |
| FB/Einrichtung: | FB 10: Mathematik und Informatik |
| Dokumenttypen: | Dissertation/Habilitation |
| Medientypen: | Text |
| Erscheinungsdatum: | 2011 |
| Publikation in MIAMI: | 26.07.2011 |
| Datum der letzten Änderung: | 31.05.2016 |
| Angaben zur Ausgabe: | [Electronic ed.] |
| Schlagwörter: | Model-Checking; Programmanalyse; Nebenläufigkeit; Monitore; dynamische Pushdown-Netzwerke; Vorgängermengen |
| Fachgebiet (DDC): | 004: Datenverarbeitung; Informatik
510: Mathematik |
| Lizenz: | InC 1.0 |
| Sprache: | English |
| Format: | PDF-Dokument |
| URN: | urn:nbn:de:hbz:6-43459441169 |
| Permalink: | https://nbn-resolving.de/urn:nbn:de:hbz:6-43459441169 |
| Onlinezugriff: | 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.