Compositional Predicate Abstraction from Game Semantics

ional Predicate Abstraction from Game Semantics Adam Bakewell and Dan R. Ghica University of Birmingham, U.K. We introduce a technique for using conventional predicate abstraction methods to reduce the state-space of models produced using game semantics. We focus on an expressive procedural language that has both local store and local control, a language which enjoys a simple game-semantic model yet is expressive enough to allow non-trivial examples. Our compositional approach allows the verification of incomplete programs (e.g. libraries) and offers the opportunity for new heuristics for improved efficiency. Game-semantic predicate abstraction can be emn an abstraction-refinement cycle in a standard way, resulting in an improved version of our experimental model-checking tool Mage, and we illustrate it with several toy examples.

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Adam Bakewell, Dan R. Ghica
• Keywords: Algorithms, Ional Predicate Abstraction, Predicate Abstraction, Predicate Abstraction Methods, TACAS 2009