Constraint-Based Abstraction of a Model Checker for Infinite State Systems

Gourinath Banda, John Patrick Gallagher

Research output: Contribution to conferencePaperResearchpeer-review

Abstract

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.
Original languageEnglish
Publication date2009
Number of pages16
Publication statusPublished - 2009
Event23rd Workshop on Constraint Logic Programming (WLP 2009) - Potsdam, Germany
Duration: 15 Sep 200916 Sep 2009

Conference

Conference23rd Workshop on Constraint Logic Programming (WLP 2009)
CountryGermany
CityPotsdam
Period15/09/200916/09/2009

Keywords

  • Model checking
  • Program analysis
  • Abstract Interpretation

Cite this

Banda, G., & Gallagher, J. P. (2009). Constraint-Based Abstraction of a Model Checker for Infinite State Systems. Paper presented at 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Germany.