Please use this identifier to cite or link to this item: doi:10.22028/D291-25864
Title: A uniform constraint-based framework for the verification of infinite state systems
Author(s): Mukhopadhyay, Supratik
Language: English
Year of Publication: 2000
SWD key words: Unendlicher Zustandsraum
Verifikation
Computerunterstütztes Verfahren
Constraint-Erfüllung
Free key words: automatic verification
infinite state system
constraint-based framework
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: Automatic verification of infinite state systems is an important area of research. Unlike its finite state counterpart, in spite of the existence of a large body of theoretical and practical results on automatic verification of infinite state systems, there does not exist a uniform framework that is applicable to a large class of systems and that facilitates description of procedures that solves the verification problem for infinite state systems in practice as well as providing tools for reasoning about the termination conditions of such procedures. The purpose of this dissertation is to provide a uniform framework that (1) allows description of infinite state systems at their own level of granularity, (2) allows specifying their properties at a high level, (3) allows description of procedures, that can solve in practice the verification problems for infinite state systems, in a declarative fashion, (4) provides tools to reason about the termination conditions for such procedures, (5) facilitates derivation of abstractions for verification as well as easy incorporation of optimization techniques, (6) allows clear separation of the logical aspects of verification from the combinatorial ones, (7) allows combination of deductive (proof-theoretic) methods with model-theoretic ones and (8) provides, for free, data structures for implicit representation of possibly infinite sets of states.
Link to this record: urn:nbn:de:bsz:291-scidok-11815
hdl:20.500.11880/25920
http://dx.doi.org/10.22028/D291-25864
Advisor: Podelski, Andreas
Date of oral examination: 10-Jan-2001
Date of registration: 6-Jul-2007
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
Dissertation_7472_Mukh_Supr_2000.pdf1,16 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.