论文部分内容阅读
广义符号轨迹赋值（Symbolic Trajectory Evaluation）引入了符号变量和抽象技术,解决了验证中状态爆炸的问题,但是却为寻找反例制造了很多障碍。针对此,提出了一种高效的寻找反例的算法,它应用集合的概念,通过回溯在父子路径之间进行集合的交集,可以高效地解决抽象引起的问题。并对此算法进行改进,解决了符号变量带来的问题。