Steenken, Dominik: Verification of infinite-state graph transformation systems via abstraction. 2015
Inhalt
- Introduction
- Basic Definitions for Verifying Graph Transformation Systems
- Abstracting Graph Transformation Systems using Three-Valued Logic
- Motivation
- Logical Encoding of Graphs
- Three-Valued Logic
- Shapes and Embedding
- Abstract Transformation and State Space Construction
- Refinement Using Shape Constraints
- SMT Encoding of Graph Embeddings and Traces
- Motivation
- Satisfiability Modulo Theories
- Encoding of a Graph
- Encoding of a Graph Embedded Into a Shape
- Encoding of a Trace
- Encoding of a Rule Application
- Encoding of the Emptiness of a Shape
- Lazy State Space Construction
- The Principle of Lazy State Space Construction
- Shape Transition Trees
- Basic Construction Loop of an STT
- Interpolation-guided Refinement Loop
- Error Analysis and Conditions on Refinement
- Automatic Abstraction Refinement via the Trace Encoding
- Manual Abstraction Refinement Supported by Soundness Checks
- Implementation: Shape Graph Analyzer
- Conclusion
- Appendix Proofs
- Appendix Code Listings
- References