Benutzer: Gast  Login
Originaltitel:
Model-Checking Pushdown Systems 
Übersetzter Titel:
Model-Checken von Pushdown Systemen 
Jahr:
2002 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Brauer, Wilfried (Prof. Dr. Dr. h.c.) 
Gutachter:
Esparza Estaun, Francisco Javier (Prof. Dr.); Rajamani, Sriram (Ph.D.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
model checking; pushdown systems; verification; linear-time logic; LTL; procedures; recursion 
Übersetzte Stichworte:
Model-Checker; Pushdown-Systeme; Verifikation; LTL; Prozeduren; Rekursion 
Schlagworte (SWD):
Kellerautomat; Verifikation; Model checking; Rekursive Funktion 
TU-Systematik:
DAT 325d; DAT 706d; DAT 542d 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
03.12.2002 
Dateigröße:
970947 bytes 
Seiten:
212 
Letzte Änderung:
11.03.2010