计算机科学 ›› 2013, Vol. 40 ›› Issue (Z6): 99-102.
徐亮,余建平
XU Liang and YU Jian-ping
摘要: 近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。
[1] Clarke E M,Emerson A.Design and synthesis of synchronization skeletons using branching-time temporal logic [C]∥Lecture Notes in Computer Science.1981,131:52-71 [2] Clarke E M,Grunberg O,Peled D A.Model Checking [M].MIT Press,1999 [3] Biere A,Cimatti A,Clarke E,et al.Symbolic model checkingwithout BDDs [C]∥Proc.of TACAS 99.1999:193-207 [4] Biere A,Cimatti A,Clarke E,et al.Symbolic Model Checking using SAT procedures instead of BDDs [C]∥Proc.of DAC 99.1999:317-320 [5] Bryant R E.Graph-based algorithms for Boolean function manipulation [J].IEEE Transactions on Computers,1986,35(12):1035-1044 [6] McMillan K L.Symbolic Model Checking [M].Kluwer Academic Publishers,Boston,1993 [7] Coudert O,Madre J C.A unified framework for the formal verification of sequential circuits [C]∥Proc.ICCAD 90.1990:126-129 [8] Emerson E A,Clarke E M.Using branching-time temporal logics to synthesize synchronization skeletons [J].Science of Computer Programming,1982,2(3):241-266 [9] Penczek W,Wozna B,Zbrzezny A.Bounded Model Checking for the Universal Fragment of CTL [J].Fundamenta Informaticae,2002,51(1/2):135-156 [10] Zhang Wen-hui.Verification of ACTL Properties by BoundedModel Checking [C]∥EUROCAST 2007.Lecture Notes in Computer Science.2007,4739:556-563 [11] Xu Yan-yan,Chen Wei,Xu Liang,et al.Evaluation of SAT-based Bounded Model Checking of ACTL Properties [C]∥Proceedings of the 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering.2007:339-348 [12] Xu Liang,Chen Wei,Xu Yan-yan,et al.Improved BoundedModel Checking for Universal Fragment of CTL [J].Journal of Computer Science and Technology,2009,24(1):96-109 [13] 徐亮.限界模型检测方法及其应用[D].北京:中国科学院研究生院,2009 [14] Pieprzyk J,Qu Cheng-xin.Rotation-Symmetric Functions andFast Hashing [C]∥Proc.of ACISP 98.1998:169-180 [15] de Moura L,Ruess H,Sorea M.Bounded Model Checking and Induction:From Refutation to Verification [C]∥Proc.of CAV 2003.2003:14-26 [16] Jhala R,McMillan K L.Interpolation and SAT-Based ModelChecking [C]∥Proc.of CAV 2003.2003:1-13 [17] Xu Liang.SMT-based Bounded Model Checking for Real-time Systems [C]∥Proceedings of the Eighth International Conference on Quality Software.2008:120-125 [18] Xu Liang.Improved SMT-based Bounded Model Checking forReal-time Systems [J].Journal of Software,2010,21(7):1491-1502 |
No related articles found! |
|