基于广义符号轨迹赋值模型验证的反例的产生

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