Abstract. This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prov...
Abstract—Symbolic Trajectory Evaluation is an industrialstrength verification method, based on symbolic simulation and abstraction, that has been highly successful in data path ...
Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham