计算机科学 ›› 2013, Vol. 40 ›› Issue (Z6): 77-86.
侯刚,周宽久,勇嘉伟,任龙涛,王小龙
HOU Gang,ZHOU Kuan-jiu,YONG Jia-wei,REN Long-tao and WANG Xiao-long
摘要: 模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。
[1] Clarke E,Emerson E.Design and synthesis of synchronization skeletons using branching time temporal logic [C]∥Procee-dings of Logic of Programs,1981,5000(131):52-71 [2] Queille J,Sifakis J.Specification and verification of concurrent systems in CESAR[C]∥Proceedings of the 5th Colloquium on International Symposium on Programming.LNCS 137,1982:337-351 [3] Clarke E,Filkorn T,Jha S.Exploiting symmetry in temporallogic model checking[C]∥Courcoubetis C,ed.Proceedings of the 5th Int’l Conf.on Computer-Aided Verification.LNCS 697,1993:450-461 [4] Emerson E,Sistla A.Symmetry and model checking[C]∥Proceedings of the 5th Int’l Conf.on Computer-Aided Verification.LNCS 697,1993:105-131 [5] Norris I C,Dill D.Better verification through symmetry[J].Formal Methods in System Design,1996,9(1/2):41-75 [6] Sistla A,Godefroid P.Symmetry and reduced symmetry in mo-del checking[C]∥CAV.LNCS 2102,2001:91-103 [7] Iosif R.Symmetry reduction criteria for software model checking[C]∥Proceedings of SPIN Workshop.LNCS 2318,2002:22-41 [8] Bosnacki D.A light-weight algorithm for model checking with symmetry reduction and weak fairness[C]∥SPIN.LNCS 2648,2003:89-103 [9] Emerson E,Wahl T.Dynamic symmetry reduction[C]∥Proceedings of Tools and Algorithms for the Construction and Analysis of Systems.LNCS 3440,2005:382-396 [10] Miller A,Donaldson A,Calder M.Symmetry in temporal logic model checking[J].ACM Computing Surveys,2006,38(3):1-36 [11] Wahl T.Adaptive symmetry reduction[C]∥Proceedings ofComputer Aided Verification(CAV’07).LNCS 4590,2007:393-405 [12] Fernandez J,Bozga M,Ghirvu L.State space reduction based on live variables analysis[J].Journal of Science of Computer Programming(SCP),2003,47(2/3):203-220 [13] Self J,Mercer E.On-the-fly dynamic dead variable analysis[C]∥Proceedings of SPIN Workshop.LNCS 4595,2007:113-130 [14] Hatcliff J,Dwyer M,Zheng H.Slicing software for model construction[J].Higher Order Symbol.Comput,2000,13(4):315-353 [15] Dwyer M,Hatcliff J,Hoosier M,et al.Evaluating the effectiveness of slicing for model reduction of concurrent object oriented programs[C]∥Proceedings of Tools and Algorithms for the Construction and Analysis of Systems.LNCS 3920,2006:73-89 [16] Overman W.Verification of Concurrent Systems Function andTiming[D].UCLA,1981 [17] Peled D.Combining partial order reductions with on-the-flymodel-checking [C]∥Proceedings of Computer Aided Verification(CAV 1994).LNCS 818,1994:377-390 [18] Holzmann G,Peled D.An improvement in formal verification[C]∥Proceedings of Formal Description Techniques VII.LNCS 234,1994:197-211 [19] Godefroid P.Partial-order methods for the verification of concurrent systems--an approach to the state-explosion problem [J].LNCS,1996,1032:212-220 [20] Penczek W,Szreter M,Gerth R,et al.Improving partial orderreductions for universal branching time properties [J].Fundamenta Informaticae,2000,43(1-4):245-267 [21] Gueta G,Flanagan C,Yahav E,et al.Cartesian partial-order reduction[C]∥Proceedings of SPIN Workshop.LNCS 4595,2007:95-112 [22] Gueta G,Flanagan C,Yahav E,et al.Cartesian Partial-OrderReduction [C]∥Computer Science.LNCS 4595,2007:112-115 [23] Wang C,Yang Z,Kahlon V,et al.Peephole Partial Order Reduction [C]∥Computer Science.2008,4963:382-396 [24] Dong Y,Ramakrishnan C.An optimizing compiler for efficientmodel checking[C]∥Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification.Testing and Verification,1999:241-256 [25] Kurshan R,Levin V,Yenigün H.Compressing transitions for model checking [C]∥Proceedings of Computer Aided Verification(CAV 2002).LNCS 2404,2002:569-581 [26] Ozdemir K,Ural H.Protocol validation by simultaneous reachability analysis [J].Computer Communications,1997,20:772-788 [27] Pnueli.In Transition From Global to Modular Temporal Reasoning about Programs [M].Logics and models of concurrent systems,1985:123-144 [28] Grumberg O,Long D.Model checking and modular verification [J].ACM Transactions on Programming Languages and Systems,1994,16(3):843-871 [29] Krimm J P,Mounier L.Compositional state space generationfrom Lotos programs[C]∥Proceedings of Tools and Algorithms for the Construction and Analysis of Systems(TACAS 1997).LNCS 1217,1997:239-258 [30] 汤宪飞,蒋昌俊,丁志军,等.基于Petri网的语义Web服务自动组合方法[J].软件学报,2007,12(1):2991-3000 [31] 文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验[J].软件学报,2007,18(6):1270-1281 [32] Berezin S,Ser C,Clarke E M[C]∥Compositional reasoning in model checking.LNCS 1536,1998:81-102 [33] Henzinger TA,Qadeer S,Rajamani S K,et al.An assume-guarantee rule for checking simulation[J].ACM Trans.on Programming Languages and Systems,2002,24(1):51-64 [34] Cobleigh J,Giannakopou D,Pasareanu C.Learning Assumptions for Compositional Verification[C]∥Proceedings of 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS2003).LNCS,2003:331-346 [35] McMillan K.Parameterized Verification of the Flash Cache Coherence Protocol by Compositional Model Checking[C]∥Correct Hardware Design and Verification Methods(ChARME 2001).Springer,2001:2144 [36] McMillan K.Verication of an Implementation of Tomasulo’sAlgorithm by Compositional Model Checking[C]∥Proceedings of 10th Conference on Computer-aided Verication(CAV 98).LNCS 1427,1998:100-121 [37] Gurov D,Huisman M,Sprenger C.Compositional verification of sequential programs with procedures [J].Information and Computation,2008,206:840-868 [38] Ahrendt W,Dylla M.A system for compositional verification of asynchronous objects [J].Science of Computer Programming,2012,77(12):1289-1309 [39] Gregoire J.State space compression in spin with GETSs[C]∥Proceedings of Second SPIN Workshop.Rutgers University,New Jersey,1996 [40] Visser W.Memory efficient state storage in SPIN[C]∥Procee-dings of SPIN Workshop.1996:21-35 [41] Larsen K,Larsson F,Pettersson P,et al.Efficient verification of real-time systems:Compact data structure and state-space reduction [C]∥Proceedings of Real-Time Systems Symposium(RTSS’97).IEEE Computer Society Press,1997:14-24 [42] Parreaux B.Difference compression in spin[C]∥Proceedings of Workshop on automata theoric verification with the SPIN model checker(SPIN’98). IEEE Computer Society Press,1998:25-29 [43] Geldenhuys J,e Villiers P.Runtime efficient state compaction in SPIN[C]∥Proceedings of SPIN Workshop.LNCS 1680,1999:12-21 [44] Geldenhuys J,Valmari A.A nearly memory-optimal data structure for sets and mappings[C]∥Proceedings of Model Checking Software(SPIN). LNCS 2648,2003:136-150 [45] Godefroid P,Holzmann G,Pirottin D.State space caching revisited[C]∥Proceedings of Computer Aided Verification(CAV 1992).LNCS 663,1992:178-191 [46] Geldenhuys J.State caching reconsidered [J].SPIN,LNCS2989,2004:23-38 [47] Penna G,Intrigila B,Melatti I.et al.Exploiting transition locality in automatic verification of finite state concurrent systems [J].Software Tools for Technology Transfer(STTT),2004,6(4):320-341 [48] Christensen S,Kristensen L,Mailund T.A sweep-line method for state space exploration [C]∥Proceedings of Tools and Algorithms for Construction and Analysis of Systems(TACAS 2001).LNCS 2031,2001:450-464 [49] Mailund T,Westergaard W.Obtaining memory-efficient reach-ability graph representations using the sweep-line method [C]∥TACAS.LNCS 2988,2004:177-191 [50] Schmidt K.Automated generation of a progress measure for the sweep-line method [C]∥TACAS.LNCS 2988,2004:192-204 [51] Holzmann G,Godefroid P,Pirottin D.Coverage preserving reduction strategies for reachability analysis[C]∥Proceedings of Protocol Specification.1992 [52] Holzmann G.State Compression in SPIN[C]∥Proceedings of the Third Spin Workshop.1997 [53] Holzmann G,Puri A.A Minimized Automaton Representationof Reachable States[J].Software Tools for Technology Transfer,1999,2(3):270-278 [54] Holzmann J.An Improved Reachability Analysis Technique[J].Software Practice and Experience,1998,18(2):137-161 [55] Holzmann J.An Analysis of Bitstate Hashing[J].Formal meth-ods in system design,1998,13(3):287-307 [56] Wolper P,Leroy D.Reliable Hashing without Collision Detection[C]∥Proceedings of the 5th International Conference Aided Verification.LNCS 697,1993:59-70 [57] Stern U,Dill D.Improved Probabilistic Verification by HashCompaction[C]∥Proceedings of IFIP WG 10.5Advanced Research Workshop on Correct Hardware Design and Verification Methods.IFIP,LNCS 987,1995:206-224 [58] Garavel H,Mateescu R,Smarandache I.Parallel state space construction for model- checking[C]∥Proceedings of SPIN Workshop.LNCS 2057,2001:217-234 [59] Lerda F,Sisto R.Distributed-memory model checking withSPIN[C]∥Proceedings of SPIN workshop.LNCS 1680,1999:22-39 [60] Lerda F,Visser W.Addressing dynamic issues of program model checking[C]∥Proceedings of SPIN Workshop.LNCS 2057,2001:80-102 [61] Barnat J,Brim L,Stˇr′lbrn′a J.Distributed LTL model-checking in SPIN[C]∥Proceedings of SPIN Workshop on Model Checking of Software.LNCS 2057,2001:200-216 [62] Barnat J,Brim L,ˇ Cern′a I.Property driven distribution of nested DFS [C]∥Proceedings of Workshop on Verification and Computational Logic.DSSE Technical Report,2002:1-10 [63] Barnat J,Brim L,Chaloupka J.Parallel breadth-first search LTL model checking[C]∥Proceedings of Automated Software Engineering(ASE’03).2003:106-115 [64] Cern′a I,Pel′anek R.Distributed explicit fair cycle detection[C]∥Proceedings SPIN workshop.LNCS 2648,2003:49-73 [65] Barnat J,Brim L,Chaloupka J.From distributed memory cycledetection to parallel LTL model checking[J].ENTCS,2005,133(1):21-39 [66] 孙伟,马绍汉.分布式博弈树搜索算法[J].计算机学报,1995,18(1):39-45 [67] Barnat J,Brim L,Rockai P.Scalable multi-core ltl model-checking[C]∥Proceedings of SPIN Workshop.LNCS 4595,2007:187-203 [68] Holzmann G,Bosnacki D.The design of a multicore extension ofthe spin model checker[J].IEEE Transactions on Software Engineering,2007,33(10):659-674 [69] Groce A,Visser W.Heuristics for model checking java programs[J].Software Tools for Technology Transfer(STTT),2004,6(4):260-276 [70] Kuehlmann A,McMillan K,Brayton R.Probabilistic state space search[C]∥Proceedings of Computer-Aided Design(CAD 1999).1999:574-579 [71] Zhou Kuan-jiu,Wang Xiao-long,Hou Gang,et al.Software Reliability Test Based on Markov Usage Model[J].Journal of Software,2012,7(9):2061-2068 [72] Sivaraj H,Gopalakrishnan G.Random Walk Based Heuristic Al-gorithms for Distributed Memory Model Checking[J].Electronic Notes in Theoretical Computer Science,2003,89:51-67 [73] Haslum P.Model checking by random walk[C]∥Proceedings of ECSEL Workshop.1999 [74] Pel′R anek,Hanˇzl T,ˇ Cern′a I,et al.Enhancing random walk state space exploration[C]∥Proceedings of Formal Methods for Industrial Critical Systems(FMICS’05).2005:98-105 [75] Jones M,Sorber J.Parallel search for LTL violations [J].Software Tools for Technology Transfer(STTT),2005,7(1):31-42 [76] Holzmann G.Algorithms for automated protocol verification[J].AT&T Technical Journal,1990,69(2):32-44 [77] Lin F,Chu P,Liu M.Protocol verification using reachability analysis:the state space explosion problem and relief strategies[J].Computer Communication Review,1987,17(5):126-134 [78] Mihail M,Papadimitriou C.On the random walk method for protocol testing [C]∥Proceedings of Computer Aided Verification(CAV 1994).LNCS 818,1994:132-141 [79] Holzmann G.An analysis of bitstate hashing[C]∥Proceedings of Protocol Specification.1995,13:301-314 [80] Dillinger P,Manolios P.Fast and accurate bitstate verification for SPIN[C]∥Proceedings of SPIN workshop.LNCS 2989,2004:57-75 [81] Dillinger P,Manolios P.Bloom filters in probabilistic verification [C]∥Proceedings of Formal Methods in Computer-Aided Design(FMCAD).LNCS 3312,2004:367-381 [82] Dillinger P,Manolios P.Enhanced Probabilistic Verification with 3Spin and 3Murphi [C]∥Model Checking Software Lecture Notes.Computer Science 3639,2005:272-276 [83] McMillan,Burch,Jerry R.Symbolic model checking for sequential circuit verification[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,1994,13(1):401-424 [84] Lee C Y.Representation of switching circuits by binary-decision programs[J].Bell Technical Journal,1959,38(4):985-999 [85] Bryant R E.Graph-based algorithms for boolean function manipulation[J].IEEE Transactions on Computers,1986,35(8):677-691 [86] Strehl K,Thiele L.Interval diagram for efficient symbolic verification of process networks[J].IEEE Trans on Computer Aided Design of Integrated Circuits and Systems,2000,19(8):939-956 [87] Moller J,Lichtenberg J,Anderson H R,et al.Difference Deci-sion Diagrams[C]∥Proc of Annunal Conf of the European Association for Computer Science Logic.1999:112-126 [88] Campos S,Clarke E,Marrero W,et al.Timing analysis of industrial real-time systems[C]∥Proc of 1st workshop on industrial Strength Formal Specification Techniques.Boca Raton,Florida,1995:97-106 [89] Okawa Y,Yoneda T.Symbolic CTL model checking of time petri nets[J].Electronics and Communications in Japan,1997,80(4):11-20 [90] Anderson R J.Beam P,Burns S,et al.Model checking large software specifications[C]∥Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering San Francisco CA.USA,1996:156-166 [91] Corte L A,Eles P,Peng Z.Formal coverification of embeddedsystems using model checking[C]∥Proc of 26th EUROM ICRO Conference.The Netherlanda,2000:106-113 [92] Laiy T,Pedram M,Vrudhulas B K.BDD based decomposition of logic functions with application to FPGA synthesis[C]∥Des Autom Conf.1993:642-647 [93] Sieling D.The Nonapproximability of OBDD minimization[J].Information and Computation,2002,172(1):103-138 [94] 闫华,张伟,赵海燕,等.基于二分决策图的特征模型验证方法[J].软件学报,2010,21(1):84-97 [95] Davis M,Logemann G,Loveland D.A Machine Program forTheorem Proving[J].Communications of the ACM,1962,5(7):394-397 [96] Zhang Han-tao.SATO:an Efficient Propositional Prover[C]∥Proceedings of the 14th International Conference on Automated Deduction(CADE-97).London,UK,1997:272-275 [97] Freeman J W.Improvements to Propositional Satisfiability Sea-rch Algorithms[D].University of Pennsylvania.Philadelphia,PA,USA,1995 [98] Marques-Silva J P,Sakallah K A.GRASP:A new search algorithm for satisfiability[C]∥Proceedings of the ACM/IEEE International Conference on Computer-Aided Design.Washington,DC,USA,1996:220-227 [99] Een N,Sorensson N.An Extensible SAT-solver[C]∥Theory and Applications of Satisfiability Testing.Santa Margherita Ligure,Italy,2003:502-518 [100] Moskewicz M,Madigan C,Zhao,et al.Chaff:Engineering an Efficient SAT Solver [C]∥Proceedings of 38th Conference on Design Automation.Las Vegas,NV,USA,2001:530-535 [101] Goldberg E,Novikov Y.BerMin:A fast and robust SAT-solver[C]∥Proceedings of Design Automation and Test in Europe(DATE).Paris,France,2002:142-149 [102] Selman B,Levesque H,Mitchell D.A new method for solving hard satisfiability problems[C]∥Proceedings of the 10th AAAI’92.Menlo Park,CA:AAAI Press,1992:440-446 [103] Selman B,Kautz H A,Cohen.Noise strategies for improving local search[C]∥Proceedings of the 12th AAAI’94.Menlo Park,CA:AAAI Press,1994:337-343 [104] McAllester D,Selman B,Kautz H.Evidence for invariants in local search[C]∥Proceedings of the 14th AAAI’97.Menlo Park,CA:AAAI Press,1997:321-326 [105] Mazure B,Sais L,Gregoire E.Tabu search for SAT[C]∥Proceedings of the 14th AAAI’97.Menlo Park,CA:AAAI Press,1997:281-285 [106] Schuurmans D,Southey F.Local search characteristics of incomplete SAT procedures[J].Artificial Intelligence,2001,132(2):121-150 [107] Prestwich S,Lynce I.Local Search for Unsatisfiability[C]∥Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing.Seattle,WA,USA,2006:283-296 [108] Audemard G,Simon L.GUNSAT:A Greedy Local Search Algorithm for Unsatisfiability[C]∥Proceedings of the 20th International Joint Conference of Artificial Intelligence.Hyderabad,India,2007:2256-2261 [109] Biere A,Cimatti A,Clarke E M,et al.Symbolic model checking without BDDs[C]∥Proceedings of the 5th Int’l Conf.on Tools and Algorithms for the Constructions and Analysis of Systems(TACAS’99).LNCS 1579,Berlin:Springer-Verlag,1999:193-207 [110] Cimatti A,Clarke E M,Giunchiglia E,et al.NuSMV2:An open source tool for symbolic model checking[C]∥Brinksma E,Larsen K G,eds.Proceedings of the 14th Int’l Conf.on Computer Aided Verification(CAV 2002).LNCS 2404,Berlin:Springer-Verlag,2002:359-364 [111] Amla N,Kurshan R,McMillan K,Medel R.Experimental analysis of different techniques for bounded model checking[C]∥Hubert G,Hatcliff J,eds.Proceedings of the 9th Int’l Conf.on Tools and Algorithms for the Constructions and Analysis of Systems(TACAS 2003).LNCS 2619,Berlin:Springer-Verlag,2003:34-48 [112] Cimatti A,Pistore M,Roveri M,et al.Improving the encoding of LTL model checking into SAT[C]∥Agostino C,ed.Procee-dings of the 3rd Int’l Workshop on Verification,Model Checking,and Abstract Interpretation(VMCAI 2002).LNCS 2294,Berlin:Springer-Verlag,2002:196-207 [113] Frisch A,Sheridan D,Walsh T.A fixpoint encoding for bounded model checking[C]∥Aagaard MD,OLeary J W,eds.Procee-dings of the 4th Int’l Conf.on Formal Methods in Computer-Aided Design(FMCAD 2002).LNCS 2517,Berlin:Springer-Verlag,2002:238-255 [114] Latvala T,Biere A,Heljanko K,et al.Simple bounded LTLmodel checking[C]∥Hu AJ,Martin AK,eds.Proceedings of the 5th Int’l Conf.on Formal Methods in Computer-Aided Design(FMCAD 2004).LNCS 3312,Berlin:Springer-Verlag,2004:186-200 [115] 杨晋吉,苏开乐,骆翔宇,等.有界模型检测的优化[J].软件学报,2009,20(8):2005-2014 [116] Jackson P,Sheridan D.Clause form conversions for boolean circuits[C]∥Hoos HH,Mitchell DG,eds.Proceedings of the 7th Int’l Conf.on Theory and Applications of Satisfiability Testing(SAT 2004).LNCS 3542,Berlin:Springer-Verlag,2004:183-198 [117] Jackson P,Sheridan D.The optimality of a fast CNF conversion and its use with SAT[C]∥Hoos HH,Mitchell DG,eds.Proceedings of the 7th Int’l Conf.on Theory and Applications of Satisfiability Testing(SAT 2004).LNCS 3709,Berlin:Springer-Verlag,2005:827-831 [118] Strichman O.Accelerating bounded model checking of safetyproperties[J].Formal Methods in System Design,2004,24(1):5-24 [119] Yokoo M,Suyama T,Sawada H.Solving Satisfiability Problems Using Field Programmable Gate Arrays:First Results[C]∥Proceedings of the Second International Conference Principles and Practice of Constraint Programming.Cambridge,Massachusetts,USA,1996:497-509 [120] Zhong P,Martonosi M,Ashar P,et al.Using Configurable Computing to Accelerate Boolean Satisfiability[J].IEEE Trans.Computer-Aided Design of Integrated Circuits and Systems,1999,18(6):861-868 [121] Abramovici M,Saab D.Satisfiability on Reconfigurable Hardware[C]∥Proceedings of Seventh International Workshop Field-Programmable Logic and Applications.London,UK,1997:448-456 [122] Dandalis A,Prasanna V K.Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers[J].ACM Trans.Design Automation of Electronic Systems,2002,7(4):547-562 [123] Sousa J,Marques-Silva J P,Abramovici M.A Configware/ Software Approach to SAT Solving[C]∥Proceedings of the Ninth IEEE International Symposium Field-Programmable Custom Computing Machines.Rohnert Park,California,USA,2001 [124] Reis N A,Sousa J.On Implementing a Configware[C]∥Software SAT Solver Proceedings of 10th IEEE International Symposium Field-Programmable Custom Computing Machines.Napa,CA,USA,2002:282-283 [125] Skliarova I,Ferrari A B.A Software/Reconfigurable Hardware SAT Solver[J].IEEE Trans.Very Large Scale Integration(VLSI) Systems,2004,12(4):408-419 [126] Kestur,Davis S,Williams J D.BLAS Comparison on FPGA,CPU and GPU[C]∥VLSI(ISVLSI).IEEE Computer Society Annual Symposium.Lixouri Kefalonia,Greece,2010:288-293 [127] 周进,赵希顺.基于硬件可编程逻辑(FPGA)的SAT算法综述[J].电子世界,2012,6:61-69 [128] Luo Zhong-wen,Yang Zheng-ping,Liu Hongzhi,et al.GA Computation of 3-SAT problem on Graphic Process Unit[C]∥Proceedings of the International Symposium on Intelligent Computation and its Application.Wuhan,Hubei,2005:27-31 [129] Luo Zhong-wen,Liu Hong-zhi.Cellular genetic algorithms and local search for 3-SAT problem on graphic hardware[C]∥Proceedings of 2006IEEE Congress on Evolutionary Computation.Vancouver,Canada,2006:2988-2992 [130] Armando A,Mantovani J,Platania L.Bounded model checking of software using SMT solvers instead of SAT solvers[J].International Journal on Software Tools for Technology Transfer,2009,11(1):69-83 [131] Cordeiro L,Fischer B,Marques-Silva J.SMT-based boundedmodel checking for embedded ANSI-C software[C]∥Procee-dings of the 2009IEEE/ACM International Conference on Automated Software Engineering.Auckland,New Zealand,2009:137-148 [132] Ganai M,Gupta A.Accelerating high-level bounded model checking[C]∥ICCAD.San Jose,CA,USA,2006:794-801 [133] 徐亮.改进的以SMT 为基础的实时系统限界模型检测[J].软件学报,2010,21(7):1491-1502 [134] Clarke E M,Grumberg O,Long D E.Model checking and abstraction[J].ACM Transactions on Programming Languages and System(TOPLAS),1994,16(5):1512-1542 [135] Dams D,Gerth R,Grumberg O.Abstract interpretation of reactive systems[J].ACM Transactions on Programming Languages and System(TOPLAS),1997,19(2):253-291 [136] Clarke E M,Grumberg O,Jha S.Counterexample-Guided abstraction Refinement for symbolic Model checking[J].Journal of the ACM,2003,50(5):752-794 [137] 袁志斌,徐正权,王能超.软件模型检测中的抽象[J].计算机科学,2006,33(7):276-279 [138] Graf S,Saidi H.Construction of abstract state graphs with PVS[C]∥Proceedings of 9th International Conference on Computer Aided Verification.Haifa,Israel,1997:72-83 [139] Colon M,Uribe T.Generating finite-state abstractions of reactive systems using decision procedures[C]∥Computer Aided Verification.Vancouver,Canada,1998:293-304 [140] Ball T,Podelski A,Rajamani S K.Boolean and Cartesian Abstraction f or Model Checking C Programs[C]∥Proceedings of Tools and Algorithms f or the Construction and Analysis of Systems.Genova,Italy,2001:268-283 [141] Ball T,Majumdar R,Millstein T,et al.Automatic Predicate Abstraction of C Programs[C]∥Proceedings of the Conference on Programming Language Design and Implementation.Snowbird,Utah,2001:203-213 (下转第111页)(上接第86页) [142] Das S,Dill D L,Park S.Experience with predicate abstraction[C]∥Computer-Aided Verification.Trento,Italy,1999:160-171 [143] Lahiri S K,Nieuwenhuis R,Oliveras A.SMT techniques for fast predicate abstraction[C]∥Proceedings of 18th International Conference on Computer Aided Verification(CAV).Seattle,USA,2006:424-437 [144] Cavada R,Cimatti A,Franzen A,et al.Computing Predicate Abstractions by Integrating BDDs and SMT Solvers[C]∥Seventh International Conference on Formal Methods in Computer-Aided Design.Austin,Texas,2007:69-76 [145] 何炎祥,吴伟,陈勇,等.基于SMT求解器的路径敏感程序验证[J].软件学报,2012,23(10):2655-2664 [146] Clarke E M,Grumberg O,Jha S,et al.Counterexample-Guided Abstraction Refinement[C]∥CAV.Berlin,Heidelberg,2000:154-169 [147] Henzinger T A,Jhala R,Majumdar R,et al.Lazy Abstraction[C]∥Proceedings of the 29th Annual Symposium on Principles of Programming Languages.Oregon,Portland,2002:58-70 [148] Cordeiro L,Fischer B,Marques-Silva J.Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking[C]∥17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems.Oxford,England,2009:160-169 [149] Kong Wei-qiang,Shiraishi,Mizushima,et al.An SMT Approach to Bounded Model Checking of Design in State Transition Matri[C]∥Proceedings of 2010International Conference on Computational Science and Its Applications(ICCSA).2010:231-238 [150] 周宽久,杨广,柳朕,等.基于拓扑排序的数据竞争方向定位[J].计算机科学,2012,39(11):108-116 [151] Wang Jie,Cui Kai,Zhou Kuan-jiu,et al.Programmable NoCScheduling Based on Multi-core Processor[C]∥Proceedings of International Conference on Electrical and Control Engineering(ICECE).2011 [152] Lai Xiao-chen,Wang Xiao-liang,Zhou Kuan-jiu,et al.Research on method of static analysis for safety of C++program[J].International Journal of Advancements in Computing Technology,2012,4(21):337-345 |
No related articles found! |
|