Table of contents

• Introduction
• Abstraction for Vanilla GC
• Snapshot creation
• Garbage collection, index/data blob compaction
• First try at specification
• State variables
• Constraints for the model checker
• Steps in the spec
• Ignore data blobs and data blob
• Avoiding semantically same, distinct states
• Behaviour pruning using Modus Tollens
• Choose data structures of state variables wisely