Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-25864
Titel: | A uniform constraint-based framework for the verification of infinite state systems |
VerfasserIn: | Mukhopadhyay, Supratik |
Sprache: | Englisch |
Erscheinungsjahr: | 2000 |
Kontrollierte Schlagwörter: | Unendlicher Zustandsraum Verifikation Computerunterstütztes Verfahren Constraint-Erfüllung |
Freie Schlagwörter: | automatic verification infinite state system constraint-based framework |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Dissertation |
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 zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-11815 hdl:20.500.11880/25920 http://dx.doi.org/10.22028/D291-25864 |
Erstgutachter: | Podelski, Andreas |
Tag der mündlichen Prüfung: | 10-Jan-2001 |
Datum des Eintrags: | 6-Jul-2007 |
Fakultät: | MI - Fakultät für Mathematik und Informatik |
Fachrichtung: | MI - Informatik |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Dissertation_7472_Mukh_Supr_2000.pdf | 1,16 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.