Automatic Abstraction for Model Checking by Symbolic Trajectory Evaluation

Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single model-checking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called "symbolic indexing" and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically.

This is joint work with Sara Adams, Magnus Bjork, and Carl Seger.