- We address the problem of implication of assertion graphs that occur in generalized symbolic trajectory evaluation (GSTE). GSTE has demonstrated its powerful capacity in formal v...
Guowu Yang, Jin Yang, William N. N. Hung, Xiaoyu S...
Abstract. Many modern systems are designed as a set of interconnected reactive subsystems. The subsystem verification task is to verify an implementation of the subsystem against t...
Abstract. This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prov...
Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary ...
Roberto Sebastiani, Eli Singerman, Stefano Tonetta...
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
Formal and dynamic (simulation, emulation, etc.) verification techniques are both needed to deal with the overall challenge of verification. Ideally, the same specification/tes...
ng Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation Yan Chen Dept. of Computer Science Portland State University Portland, OR, 97207 chenyan@cs.pdx.e...