User: Guest  Login
Original title:
Model-Checking Pushdown Systems
Translated title:
Model-Checken von Pushdown Systemen
Author:
Schwoon, Stefan
Year:
2002
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Brauer, Wilfried (Prof. Dr. Dr. h.c.)
Referee:
Esparza Estaun, Francisco Javier (Prof. Dr.); Rajamani, Sriram (Ph.D.)
Format:
Text
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
model checking; pushdown systems; verification; linear-time logic; LTL; procedures; recursion
Translated keywords:
Model-Checker; Pushdown-Systeme; Verifikation; LTL; Prozeduren; Rekursion
Controlled terms:
Kellerautomat; Verifikation; Model checking; Rekursive Funktion
TUM classification:
DAT 325d; DAT 706d; DAT 542d
Abstract:
The thesis investigates an approach to automated software verification based on pushdown systems. Pushdown systems are, roughly speaking, transition systems whose states include a stack of unbounded length; there is a natural correspondence between them and the execution sequences of programs with (possibly recursive) subroutines. The thesis examines model-checking problems for pushdown systems, improving previously known algorithms in terms of both asymptotic complexity and practical usability...    »
Translated abstract:
Die Arbeit untersucht einen Ansatz zur automatischen Softwareverifikation, der auf Pushdown-Systemen basiert. Pushdown-Systeme sind (vereinfacht gesagt) Transitionssysteme, deren Zustände einen Keller unbegrenzter Länge beinhalten; es besteht eine natürliche Beziehung zwischen diesen Systemen und Programmen mit rekursiven Prozeduren. Die Arbeit untersucht Model-Checking-Probleme auf Pushdown-Systemen, wobei sie zuvor bekannte Algorithmen verbessert, sowohl in asymptotischer Hinsicht als auch mi...    »
Publication :
Universitätsbibliothek der TU München
WWW:
https://mediatum.ub.tum.de/?id=601720
Date of submission:
27.06.2002
Oral examination:
03.12.2002
File size:
970947 bytes
Pages:
212
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss2002120317052
Last change:
11.03.2010
 BibTeX