Eingang zum Volltext in OPUS

Home | Suche | Browsen

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:kobv:517-opus-41516
URL: http://opus.kobv.de/ubp/volltexte/2010/4151/


Banda, Gourinath ; Gallagher, John P.

Constraint-based abstraction of a model checker for infinite state systems

pdf-Format:
Dokument 1.pdf (1.789 KB) (SHA-1:4f7f180815198c1edb033e9655410db3053626fa)


Kurzfassung in Englisch

Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver.

Collection: Universität Potsdam / Tagungen / Proceedings of the 23rd Workshop on (Constraint) Logic Programming 2009 / Theory of Logic Programming
Institut: Extern
DDC-Sachgruppe: Informatik
Sonstige beteiligte Institution: Gesellschaft für Logische Programmierung e.V.
Dokumentart: c InProceedings (Aufsatz / Paper einer Konferenz etc.)
Quelle: Proceedings of the 23rd Workshop on (Constraint) Logic Programming 2009 / Geske, Ulrich; Wolf, Armin (Hrsg.). - Potsdam : Universitätsverlag, 2010. - S. 109 - 124
Sprache: Englisch
Erstellungsjahr: 2010
Publikationsdatum: 04.03.2010
Bemerkung:
Work partly supported by the Danish Natural Science Research Council project SAFT: Static Analysis Using Finite Tree Automata.
Lizenz: Diese Nutzungsbedingung gilt nicht, wenn in den Metadaten eine modifizierende Lizenz genannt ist. Keine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht


Home | Leitlinien | Impressum | Haftungsausschluss | Statistik | Universitätsverlag | Universitätsbibliothek
Ihr Kontakt für Fragen und Anregungen:
Universitätsbibliothek Potsdam
powered by OPUS  Hosted by KOBV  Open
Archives Initiative  DINI Zertifikat 2007  OA Netzwerk