计算机科学 ›› 2013, Vol. 40 ›› Issue (Z6): 77-86.

• 智能算法与优化 • 上一篇    下一篇

模型检测中状态爆炸问题研究综述

侯刚,周宽久,勇嘉伟,任龙涛,王小龙   

  1. 大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620
  • 出版日期:2018-11-16 发布日期:2018-11-16
  • 基金资助:
    本文受国家自然科学基金项目(91018003,61272174)资助

Survey of State Explosion Problem in Model Checking

HOU Gang,ZHOU Kuan-jiu,YONG Jia-wei,REN Long-tao and WANG Xiao-long   

  • Online:2018-11-16 Published:2018-11-16

摘要: 模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。

关键词: 软件系统,模型检测,状态空间爆炸,形式化验证

Abstract: Model checking has become an important approach to ensure the correctness and reliability software systems.However,with the increasingly powerful software functionality,system scale and complexity are also growing.Then it is easy to produce state explosion problem in model checking process.How to solve the state explosion in model checking has become an important issue that can not be avoided by the industry and theorists.In this paper,we overviewed the key technology and main methods of solving state explosion problem,and proposed the latest research progress and direction in this field of model checking.

Key words: Software systems,Model checking,State explosion,Formal verification

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!