User: Guest  Login
Original title:
Model-Checking Pushdown Systems 
Translated title:
Model-Checken von Pushdown Systemen 
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 
Oral examination:
03.12.2002 
File size:
970947 bytes 
Pages:
212 
Last change:
11.03.2010