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

  • 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.

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS
  • Export XML

Additional Services

Share in Twitter Search Google Scholar
Author:Gourinath Banda, John P. Gallagher
Document Type:Conference Proceeding
Year of Completion:2010
Publishing Institution:Universität Potsdam
Contributing Corporation:Gesellschaft für Logische Programmierung e.V.
Release Date:2010/03/04
Source:Proceedings of the 23rd Workshop on (Constraint) Logic Programming 2009 / Geske, Ulrich; Wolf, Armin (Hrsg.). - Potsdam : Universitätsverlag, 2010. - S. 109 - 124
Organizational units:Extern / Extern
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Collections:Universität Potsdam / Tagungen / Proceedings of the 23rd Workshop on (Constraint) Logic Programming 2009 / Theory of Logic Programming
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:
Work partly supported by the Danish Natural Science Research Council project SAFT: Static Analysis Using Finite Tree Automata.