Abstract: Symbolic Trajectory Evaluation is a model checking technology based on a form of symbolic simulation that works natively on the abstraction lattice obtained from quaternion abstraction. It tends to perform very well in term of capacity and usability on a number of problem classes. Its main drawback is the limited expressiveness of its specification language, which allows only properties over finite time intervals.

This talk will describe a generalization of STE, named—rather unimaginatively—GSTE. It allows the extension of STE style model checking to a larger class of properties, retaining STE's efficiency. GSTE comes with its own characteristic specification language called Assertion Graphs. I will describe the syntax and define the semantics of Assertion Graphs and present a simulation based model checking algorithm for them. This algorithm can naturally be adapted to work with abstraction based simulation such as STE.

Andreas Tiemeyer received a PhD in Mathematics from the University of Bielefeld. He then switched fields and has been working on Formal Verification at Intel ever since. His main interests are specification languages and model checking algorithms.