The role of model checking in software engineering

Abstract

Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts.

This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems.

The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.

Keywords

software engineering / model checking / stateexplosion

References

[1] Ben-Ari M. A primer on model checking. Inroads, 2010, 1(1): 40–47

[2] Baier C, Katoen J-P. Principles of Model Checking. Cambridge: The MIT Press, 2008

[3] Garcia-Ferreira I, Laorden C, Santos I, Bringas P G. A survey on static analysis and model checking. In: Proceeding of International Joint Conference SOCO, CISIS & ICEUTE. 2014, 443–452

[4] Andersen H R, Lind-Nielsen J. Partial model checking of modal equations: a survey. International Journal on Software Tools for Technology Transfer, 1999, 2(3): 242–259

[5] Abdulla P A, Jonsson B, Nilsson M, Saksena M. A survey of regularmodel checking. In: Proceedings of the 15th International Conference on Concurrency Theory. 2004, 35–48

[6] Edelkamp S, Schuppan V, Bosnacki D, Wijs A, Fehnker A, Aljazzar H. Survey on directed model checking. In: Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence. 2008, 65–89

[7] Bhaduri P, Ramesh S. Model checking of statechart models: survey and research directions. Computer Science, 2004

[8] Zuck L D, Pnueli A. Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures, 2004, 30(3–4): 139–169

[9] Eiter T, Gottlob G, Schwentick T. The model checking problem for prefix classes of second-order logic: a survey. In: Blass A, Dershowitz N, Reisig W, eds. Fields of Logic and Computation. Spinger International Publishing, 2010, 227–250

[10] Fraser G, Wotawa F, Ammann P. Testing with model checkers: a survey. Software Testing, Verification & Reliability, 2009, 19(3): 215–261

[11] Grumberg O, Veith H. 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 2008

[12] Clarke E M, Emerson A E. Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of Workshop on Logic of Programs. 1981, 52–71

[13] Queille J-P, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the International Symposium on Programming. 1982, 337–351

[14] Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74–84

[15] Rungta N, Mercer E G. A context-sensitive structural heuristic for guided search model checking. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2005, 410–413

[16] Letarte D. Model checking graph representation of precise Boolean inter-procedural flow analysis. In: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2010, 511–516

[17] Park D Y W, Stern U, Skakkebak J U, Dill D L. Java model checking. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE). 2000, 253–256

[18] Iosif R. Exploiting heap symmetries in explicit-state model checking of software. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE). 2001, 254–261

[19] Inverardi P, Muccini H, Pelliccione P. Automated check of architectural models consistency using SPIN. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE). 2001, 346–349

[20] Barnat J, Brim L, Chaloupka J. Parallel breadth-first search LTL model-checking. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE). 2003, 106–115

[21] Dwyer M B, Robb y, Tkachuk O, Visser W. Analyzing interaction orderings with model checking. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE). 2004, 154–163

[22] Mehlitz P C, Tkachuk O, Ujma M. JPF-AWT: model checking GUI applications. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011, 584–587

[23] Loer K, Harrison M D. Towards usable and relevant model checking techniques for the analysis of dependable interactive systems. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE). 2002, 223–226

[24] Tkachuk O, Dwyer M B, Pasareanu C S. Automated environment generation for software model checking. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE). 2003, 116–129

[25] Tkachuk O, Rajan S P. Combining environment generation and slicing for modular software model checking. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2007, 401–404

[26] Visser W, Havelund K, Brat G P, Park S. Model checking programs. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE). 2000, 3–12

[27] Brat G P, Visser W. Combining static analysis and model checking for software analysis. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE). 2001, 262

[28] Kim K, Yavuz-Kahveci T, Sanders B A. Precise data race detection in a relaxed memory model using heuristic-based model checking. In: Proceedings of IEEE/ACM International Conference on Automated Software Engineering (ASE). 2009, 495–499

[29] Kim K, Yavuz-Kahveci T, Sanders B A. JRF-E: using model checking to give advice on eliminating memory model-related bugs. In: Proceedings of the 25th IEEE International Conference on Automated Software Engineering (ASE). 2010, 215–224

[30] Heimdahl M P E, Choi Y, Whalen M W. Deviation analysis through model checking. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering. 2002 (ASE), 37–46

[31] Choi Y, Heimdahl M P E. Model checking software requirement specifications using domain reduction abstraction. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE). 2003, 314–317

[32] Xie F, Levin V, Browne J C. Model checking for an executable subset of UML. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE). 2001, 333–336

[33] Simmonds J, Bastarrica C M. A tool for automatic UML model consistency checking. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2005, 431–432

[34] Barber K S, Graser T J, Holt J. Providing early feedback in the development cycle through automated application of model checking to software architectures. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE). 2001, 341–345

[35] Robb y, Dwyer M B, Hatcli J. Domain-specific model checking using the Bogor framework. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE). 2006, 369–370

[36] Hart T E, Ku K, Gurfinkel A, Chechik M, Lie D. PtYasm: software model checking with proof templates. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2008, 479–480

[37] Witkowski T, Blanc N, Kroening D, Weissenbacher G. Model checking concurrent linux device drivers. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2007, 501–504

[38] Vakili A, Day N A. Using model checking to analyze static properties of declarative models. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011, 428–431

[39] Crhova J. Distributed modular model checking. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE). 2002, 312

[40] Artho C, Garoche P. Accurate centralization for applying model checking on networked applications. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE). 2006, 177–188

[41] Leungwattanakit W, Artho C, Hagiya M, Tanabe Y, Yamamoto M. Model checking distributed systems by combining caching and process checkpointing. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011, 103–112

[42] Artho C, Leungwattanakit W, Hagiya M, Tanabe Y, Yamamoto M. Cache-based model checking of networked applications: from linear to branching time. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2009, 447–458

[43] Artho C, Hagiya M, Potter R, Tanabe Y, Weitl F, Yamamoto M. Software model checking for distributed systems with selectorbased, non-blocking communication. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2013, 169–179

[44] Haydar M, Boroday S, Petrenko A, Sahraoui H A. Properties and scopes in Web model checking. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2005, 400–404

[45] Barnat J, Brim L, Simecek P. Cluster-based I/O-efficient LTL model checking. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2009, 635–639

[46] Halle S, Ettema T, Bunch C, Bultan T. Eliminating navigation errors in Web applications via model checking and runtime enforcement of navigation state machines. In: Proceedings of the 25th IEEE/ACMInternational Conference on Automated Software Engineering (ASE). 2010, 235–244

[47] Choi Y, Heimdahl M P E. Combination model checking: approach and a case study. In: Proceedings of the 19th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2004, 354–357

[48] Post H, Sinz C, Kaiser A, Gorges T. Reducing false positives by combining abstract interpretation and bounded model checking. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2008, 188–197

[49] Pradella M, Morzenti A, Pietro P S. Refining real-time system specifications through bounded model- and satisfiability-checking. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2008, 119–127

[50] Cho C Y, D’Silva V, Song D. BLITZ: Compositional bounded model checking for real-world programs. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2013, 136–146

[51] Cordeiro L C, Fischer B, Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2009, 137–148

[52] Nguyen T K, Sun J, Liu Y, Dong J S. A model checking framework for hierarchical systems. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011, 633–636

[53] Vierhauser M, Grunbacher P, Egyed A, Rabiser R, Heider W. Flexible and scalable consistency checking on product line variability models. In: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2010, 63–72

[54] Lauenroth K, Pohl K, Toehning S. Model checking of domain artifacts in product line engineering. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2009, 269–280

[55] Liu C, Ye E, Richardson D J. Software library usage pattern extraction using a software model checker. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE). 2006, 301–304

[56] Kim M, Kim Y, Kim H. Unit testing of flash memory device driver through a SAT-based model checker. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2008, 198–207

[57] Song F, Touili T. PuMoC: a CTL model-checker for sequential programs. In: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2012, 346–349

[58] Ku K, Hart T E, Chechik M, Lie D. A buffer overflow benchmark for software model checkers. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2007, 389–392

[59] Armando A, Benerecetti M, Carotenuto D, Mantovani J, Spica P. The EUREKA tool for software model checking. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE). 2007, 541–542

[60] Falke S, Merz F, Sinz C. The bounded model checker LLBMC. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2013, 706–709.

[61] He R, Jennings P, Basu S, Ghosh A P, Wu H. A bounded statistical approach for model checking of unbounded until properties. In: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2010, 225–234

[62] Nishi M. Towards bounded model checking using nonlinear programming solver. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE). 2016, 560–565

[63] Inverso O, Nguyen T L, Fischer B, Torre S L, Parlato G. Lazy-CSeq: a context-bounded model checking tool for multi-threaded Cprograms. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2015, 807–812

[64] Hong H S, Cha S D, Lee I, Sokolsky O, Ural H. Data flow testing as model checking. In: Proceedings of the 25th IEEE International Conference on Software Engineering (ICSE). 2003, 232–243

[65] Su T, Fu Z, Pu G, He J, Su Z. Combining symbolic execution and model checking for data flow testing. In: Proceedings of the 37th IEEE International Conference on Software Engineering (ICSE). 2015, 654–665

[66] Tian C, Duan Z. Detecting spurious counterexamples efficiently in abstract model checking. In: Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE). 2013, 202–211

[67] Kaveh N. Model checking distributd objects design. In: Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE). 2001, 793–794

[68] Sabetzadeh M, Nejati S, Easterbrook S M, Chechik M. Global consistency checking of distributed models with TReMer+. In: Proceedings of the 30th IEEE International Conference on Software Engineering (ICSE). 2008, 815–818

[69] Egyed A. UML/Analyzer: a tool for the instant consistency checking of UML models. In: Proceedings of the 29th IEEE International Conference on Software Engineering (ICSE). 2007, 793–796

[70] Bultan T. Action language: a specification language for model checking reactive systems. In: Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE). 2000, 335–344

[71] Song S, Hao J, Liu Y, Sun J, Leung H, Dong J S. Analyzing multi agent systems with probabilistic model checking approach. In: Proceedings of the 34th IEEE International Conference on Software Engineering (ICSE). 2012, 1337–1340

[72] Dong J S, Hao P, Zhang X, Qin S. HighSpec: a tool for building and checking OZTA models. In: Proceedings of the 28th IEEE International Conference on Software Engineering (ICSE). 2006, 775–778

[73] Chang F S-H, Jackson D. Symbolic model checking of declarative relational models. In: Proceedings of the 28th IEEE International Conference on Software Engineering (ICSE). 2006, 312–320

[74] Cordeiro L C. SMT-based bounded model checking for multi threaded software in embedded systems. In: Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE). 2010, 373–376

[75] Cordeiro L C, Fischer B. Verifying multi-threaded software using SMT-based context-bounded model checking. In: Proceedings of the 33rd IEEE International Conference on Software Engineering (ICSE). 2011, 331–340

[76] Classen A, Heymans P, Schobbens P-Y, Legay A, Raskin J-F. Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE). 2010, 335–344

[77] Classen A, Heymans P, Schobbens P-Y, Legay A. Symbolic model checking of software product lines. In: Proceedings of the 33rd IEEE International Conference on Software Engineering (ICSE). 2011, 321–330

[78] Ben-David S, Sterin B, Atlee J M, Beidu S. Symbolic model checking of product-line requirements using SAT-based methods. In: Proceedings of the 37th IEEE International Conference on Software Engineering (ICSE). 2015, 189–199

[79] Cordy M, Classen A, Perrouin G, Schobbens P-Y, Heymans P, Legay A. Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th IEEE International Conference on Software Engineering (ICSE). 2012, 672–682

[80] Cordy M, Schobbens P-Y, Heymans P, Legay A. Beyond Boolean product-line model checking: dealing with feature attributes and multi-features. In: Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE). 2013, 472–481

[81] Marinho F G. A proposal for consistency checking in dynamic software product line models using OCL. In: Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE). 2010, 333–334

[82] Corbett J C, Dwyer M B, Hatcli J, Robb y. Bandera: extracting finitestate models from Java source code. In: Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE). 2000, 439–448

[83] Chandra S, Godefroid P, Palm C. Software model checking in practice: an industrial case study. In: Proceedings of the 24th IEEE International Conference on Software Engineering (ICSE). 2002, 431–441

[84] Dang Z, Kemmerer R A. Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems. In: Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE). 2000, 345–354

[85] Alur R, Alfaro L, Grosu R, Henzinger T A, Kang M, Kirsch CM, Majumdar R, Mang F Y C, Wang B-Y. JMOCHA: a model checking tool that exploits design structure. In: Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE). 2001, 835–836

[86] Easterbrook S M, Chechik M, Devereux B, Gurfinkel A, Lai A Y C, Petrovykh V, Tafliovich A, Thompson-Walsh C D. XChek: a model checker for multi-valued reasoning. In: Proceedings of the 25th IEEE International Conference on Software Engineering (ICSE). 2003, 804–805

[87] Long B, Dingel J, Graham T C N. Experience applying the SPIN model checker to an industrial telecommunications system. In: Proceedings of the 30th IEEE International Conference on Software Engineering (ICSE). 2008: 693–702

[88] Dong J S, Sun J, Liu Y. Build your own model checker in one month. In: Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE). 2013, 1481–1483

[89] Chan W, Anderson R J, Beame P, Jones D H, Notkin D, Warner W E. Decoupling synchronization from local control for efficient symbolic model checking of state charts. In: Proceedings of the 21st IEEE International Conference on Software Engineering (ICSE). 1999, 142–151

[90] Su G, Rosenblum D S, Tamburrelli G. Reliability of run-time qualityof- service evaluation using parametric model checking. In: Proceedings of the 38th IEEE International Conference on Software Engineering (ICSE). 2016, 73–84

[91] Huang A. Maximally stateless model checking for concurrent bugs under relaxed memory models. In: Proceedings of the 38th IEEE International Conference on Software Engineering (ICSE). 2016, 686–688

[92] Han T, Katoen J-P, Damman B. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering, 2009, 35(2): 241–257

[93] Tian C, Duan Z, Duan Z. Making CEGAR more efficient in software model checking. IEEE Transactions on Software Engineering, 2014, 40(12): 1206–1223

[94] Moffett Y, Dingel J, Beaulieu A. Verifying protocol conformance using software model checking for the model-driven development of embedded systems. IEEE Transactions on Software Engineering, 2013, 39(9): 1307–1325

[95] Alrajeh D, Kramer J, Russo A, Uchitel S. Elaborating requirements using model checking and inductive learning. IEEE Transactions on Software Engineering, 2013, 39(3): 361–383

[96] Leungwattanakit W, Artho C, Hagiya M, Tanabe Y, Yamamoto M, Takahashi K. Modular software model checking for distributed systems. IEEE Transactions on Software Engineering, 2014, 40(5): 483–501

[97] Artzi S, Kiezun A, Dolby J, Tip F, Dig D, Paradkar A M, Ernst M D. Finding bugs in web applications using dynamic test generation and explicit-state model checking. IEEE Transactions on Software Engineering, 2010, 36(4): 474–494

[98] Santone A. Heuristic search+ local model checking in selective mucalculus. IEEE Transactions on Software Engineering, 2003, 29(6): 510–523

[99] Heitmeyer C L, Kirby J, Labaw B G, Archer M, Bharadwaj R. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 1998, 24(11): 927–948

[100] Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279–295

[101] Bang K-S, Choi J-Y, Yoo C. Comments on “The Model Checker SPIN”. IEEE Transactions on Software Engineering, 2001, 27(6): 573–576

[102] Holzmann G J, Bosnacki D. The design of a multi core extension of the SPIN model checker. IEEE Transactions on Software Engineering, 2007, 33(10): 659–674

[103] Kim M, Kim Y, Kim H. A comparative study of software model checkers as unit testing tools: an industrial case study. IEEE Transactions on Software Engineering, 2011, 37(2): 146–160

[104] Chan W, Anderson R J, Beame P, Burns S, Modugno F, Notkin D, Reese J D. Model checking large software specifications. IEEE Transactions on Software Engineering, 1998, 24(7): 498–520

[105] Chan W, Anderson R J, Beame P, Jones D H, Notkin D, Warner W E. Optimizing symbolic model checking for state charts. IEEE Transactions on Software Engineering, 2001, 27(2): 170–190

[106] Cordeiro L C, Fischer B, Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software. IEEE Transactions on Software Engineering, 2012, 38(4): 957–974

[107] Ikeda S, Jibiki M, Kuno Y. Coverage estimation in model checking with bits tate hashing. IEEE Transactions on Software Engineering, 2013, 39(4): 477–486

[108] Paolieri M, Horvath A, Vicario E. Probabilistic model checking of regenerative concurrent systems. IEEE Transactions on Software Engineering, 2016, 42(2): 153–169

[109] Su G, Feng Y, Chen T, Rosenblum D S. Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters. IEEE Transactions on Software Engineering, 2016, 42(7): 623–639

[110] Chavez H M, Shen W, France R B, Mechling B A, Li G. An approach to checking consistency between UML class model and its Java implementation. IEEE Transactions on Software Engineering, 2016, 42(4): 322–344

[111] Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T. Abstract regular tree model checking of complex dynamic data Structures. In: Proceedings of the 13th International Static Analysis Symposium (SAS). 2006, 52–70

[112] Schmidt D A, Steen B. Program analysis as model checking of abstract interpretations. In: Proceedings of the 5th International Static Analysis Symposium (SAS). 1998, 351–380

[113] Podelski A. Model checking as constraint solving. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 22–37

[114] Cleaveland R, Iyer S P, Yankelevich D. Optimality in abstractions of model checking. In: Proceedings of the 2nd International Static Analysis Symposium (SAS). 1995, 51–63

[115] Saidi H. Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 377–396

[116] Levi F. A symbolic semantics for abstract model checking. In: Proceedings of the 5th International Static Analysis Symposium (SAS). 1998, 134–151

[117] Gallardo M, Merino P, Pimentel E. Refinement of LTL formulas for abstract model checking. In: Proceedings of the 9th International Static Analysis Symposium (SAS). 2002, 395–410

[118] Monniaux D, Gonnord L. Using bounded model checking to focus fix point iterations. In: Proceedings of the 18th International Static Analysis Symposium (SAS). 2011, 369–385

[119] Giacobazzi R, Quintarelli E. Incompleteness, counterexamples, and refinements in abstract model-checking. In: Proceedings of the 8th International Static Analysis Symposium (SAS). 2001, 356–373

[120] Ranzato F, Tapparo F. Making abstract model checking strongly preserving. In: Proceedings of the 9th International Static Analysis Symposium (SAS). 2002, 411–427

[121] Wehrle M, Helmert M. The causal graph revisited for directed model checking. In: Proceedings of the 16th International Static Analysis Symposium (SAS). 2009, 86–101

[122] Fedyukovich G, D’Iddio A C, Hyvarinen A E J, Sharygina N. Symbolic detection of assertion dependencies for bounded model checking. In: Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE). 2015, 186–201

[123] Sharygina N, Browne J C. Model checking software via abstraction of loop transitions. In: Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering (FASE). 2003, 325–340

[124] Xie F, Browne J C. ObjectCheck: A model checking tool for executable object-oriented software system designs. In: Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE). 2002, 331–335

[125] Xie F, Levin V, Browne J C. Integrated state space reduction for model checking executable object-oriented software system designs. In: Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE). 2002, 64–79

[126] Saffrey P, Calder M. Optimising communication structure for model checking. In: Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE). 2004, 310–323

[127] Xie F, Levin V, Kurshan R P, Browne J C. Translating software designs for model checking. In: Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE). 2004, 324–338

[128] Fantechi A, Gnesi S, Lapadula A, Mazzanti F, Pugliese R, Tiezzi F. A model checking approach for verifying COWS specifications. In: Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering (FASE). 2008, 230–245

[129] Beyer D, Lowe S. Explicit-state software model checking based on CEGAR and interpolation. In: Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE). 2013, 146–162

[130] Mota A, Sampaio A. Model-checking CSP-Z. In: Proceedings of the 1st International Conference on Fundamental Approaches to Software Engineering (FASE). 1998, 205–220

[131] Baier C, Dubslaff C, Kluppelholz S, Daum M, Klein J, Marcker S, Wunderlich S. Probabilistic model checking and non-standard multiobjective reasoning. In: Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE). 2014, 1–16

[132] Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Proceedings of the 11th ESEC/FSE. 2003, 257–266

[133] Dwyer M B, Carr V, Hines L. Model checking graphical user interfaces using abstractions. In: Proceedings of the 5th ESEC/FSE. 1997, 244–261

[134] Tkachuk O, Dwyer M B. Adapting side effects analysis for modular program model checking. In: Proceedings of the 11th ESEC/FSE. 2003, 188–197

[135] Choi Y, Rayadurgam S, Heimdahl M P E. Automatic abstraction for model checking software systems with interrelated numeric constraints. In: Proceedings of the 9th ESEC/FSE. 2001, 164–174

[136] Gargantini A, Heitmeyer C L. Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th ESEC/FSE. 1999, 146–162

[137] Zervoudakis F, Rosenblum D S, Elbaum S G, Finkelstein A. Cascading verification: an integrated method for domain-specific model checking. In: Proceedings of the 21st ESEC/FSE. 2013, 400–410

[138] Song F, Touili T. PoMMaDe: pushdown model-checking for mal ware detection. In: Proceedings of the 21st ESEC/FSE. 2013, 607–610

[139] Liu S, Liu Y, Sun J, Zheng M, Wadhwa B, Dong J S. USMMC: a self contained model checker for UML state machines. In: Proceedings of the 21st ESEC/FSE. 2013, 623–626

[140] Robb y, Dwyer M B, Hatcliff J. Bogor: an extensible and highly modular software model checking framework. In: Proceedings of the 11th ESEC/FSE. 2003, 267–276

[141] Naik M, Palsberg J. A type system equivalent to a model checker. ACM Transactions of Programming Languages and Systems, 2008, 30(5): 29

[142] Yang J, Mok A K, Wang F. Symbolic model checking for eventdriven real-time systems. ACM Transactions of Programming Languages and Systems, 1997, 19(2): 386–412

[143] Emerson E A, Sistla A P. Utilizing symmetry when model-checking under fairness assumptions: an automata-theoretic approach. ACM Transactions of Programming Languages and Systems, 1997, 19(4): 617–638

[144] Sistla A P, Godefroid P. Symmetry and reduced symmetry in model checking. ACM Transactions of Programming Languages and Systems, 2004, 26(4): 702–734

[145] Bultan T, Gerber R, Pugh W. Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions of Programming Languages and Systems, 1997, 21(4): 747–789

[146] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions of Programming Languages and Systems, 1994, 16(5): 1512–1542

[147] Norris B, Demsky B. A practical approach for model checking C/C++11 code. ACM Transactions of Programming Languages and Systems, 2016, 38(3): 10

[148] Siegel S F, Mironova A, Avrunin G S, Clarke L A. Combining symbolic execution with model checking to verify parallel numerical programs. ACM Transactions on Software Engineering and Methodology, 2008, 17(2): 10

[149] Krishnamurthi S, Fisler K. Foundations of incremental aspect modelchecking. ACM Transactions on Software Engineering and Methodology, 2007, 16(2): 7

[150] Paige R F, Brooke P J, Ostroff J S. Metamodel-based model conformance and multiview consistency checking. ACM Transactions on Software Engineering and Methodology, 2007, 16(3): 11

[151] Basu S, Smolka S A. Model checking the Java metalocking algorithm. ACM Transactions on Software Engineering and Methodology, 2007, 16(3): 12

[152] Eshuis R. Symbolic model checking of UML activity diagrams. ACM Transactions on Software Engineering and Methodology, 2006, 15(1): 1–38

[153] Sistla A P, Gyuris V, Emerson E A. SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions on Software Engineering and Methodology, 2000, 9(2): 133–166

[154] Chechik M, Devereux B, Easterbrook S M, Gurfinkel A. Multi-valued symbolic model-checking. ACM Transactions on Software Engineering and Methodology, 2003, 12(4): 371–408

[155] Siegel S F, Mironova A, Avrunin G S, Clarke L A. Using model checking with symbolic execution to verify parallel numerical programs. In: Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 2006, 157–168

[156] Gui L, Sun J, Liu Y, Si Y J, Dong J S, Wang X. Combining model checking and testing with an application to reliability prediction and distribution. In: Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 2013, 101–111

[157] Fu X, Bultan T, Su J. Model checking XML manipulating software. In: Proceedings Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 2004, 252–262

[158] Leesatapornwongsa T, Gunawi H S. SAMC: a fast model checker for finding heisenbugs in distributed systems (demo). In: Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 2015, 423–427

[159] Chan W, Anderson R J, Beame P, Notkin D. Improving efficiency of symbolic model checking for state-based system requirements. In: Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 1998, 102–112

[160] Groce A, Visser W. Model checking Java programs using structural heuristics. In: Proceedings of ACMInternational Symposium on Software Testing and Analysis (ISSTA). 2002, 12–21

[161] Ramsay S J, Neatjerway R P, Ong C L. A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of the 41st POPL. 2014, 61–72

[162] Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd POPL. 2005, 110–121

[163] Chaki S, Rajamani S K, Rehof J. Types as models: model checking message-passing programs. In: Proceedings of the 29th POPL. 2002, 45–57

[164] Schmidt D A, Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th POPL. 1998, 38–48

[165] Godefroid P. Model checking for programming languages using Verisoft. In: Proceedings of the 24th POPL. 1997, 174–186

[166] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. In: Proceedings of the 19th POPL. 1992, 342–354

[167] Hsiung P-A, Chen Y-R, Lin Y-H. Model checking safety-critical systems using safe charts. IEEE Transactions on Computers, 2007, 56(5): 692–705

[168] He F, Song X, Hung W N N, Gu M, Sun J. Integrating evolutionary computation with abstraction refinement for model checking. IEEE Transactions on Computers, 2010, 59(1): 116–126

[169] Zheng H, Yao H, Yoneda T. Modular model checking of large asynchronous designs with efficient abstraction refinement. IEEE Transactions on Computers, 2010, 59(4): 561–573

[170] Chen Y-R, Yeh J-J, Hsiung P-A, Chen S-J. Accelerating coverage estimation through partial model checking. IEEE Transactions on Computers, 2014, 63(7): 1613–1625

[171] Zheng H, Zhang Z, Myers C J, Rodriguez E, Zhang Y. Compositional model checking of concurrent systems. IEEE Transactions on Computers, 2015, 64(6): 1607–1621

[172] Roberson M, Boyapati C. Efficient modular glass box software model checking. In: Proceedings of OOPSLA. 2010, 4–21

[173] Demsky B, Lam P. SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of OOPSLA. 2015, 20–36

[174] Jensen C S, Moller A, Raychev V, Dimitrov D, Vechev M T. Stateless model checking of event-driven applications. In: Proceedings of OOPSLA. 2015, 57–73

[175] Darga P T, Boyapati C. Efficient software model checking of data structure properties. In: Proceedings of OOPSLA. 2006, 363–382

[176] Roberson M, Harries M, Darga P T, Boyapati C. Efficient software model checking of soundness of type systems. In: Proceedings of OOPSLA. 2008, 493–504

[177] Burckhardt S, Alur R, Martin M M K. CheckFence: checking consistency of concurrent data types on relaxed memory models. In: Proceedings of PLDI. 2007, 12–21

[178] Huang J. Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of PLDI. 2015, 165–174

[179] Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI. 2011, 222–233

[180] Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of PLDI. 2008, 362–371

[181] Choi Y. Safety analysis of trampoline OS using model checking: an experience report. In: Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering (ISSRE). 2011, 200–209

[182] Liu Y, Sun J, Dong J S. PAT3: an extensible architecture for building multi-domain model checker. In: Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering (ISSRE). 2011, 190–199

[183] Kim Y J, Kim M. Hybrid statistical model checking technique for reliable safety critical systems. In: Proceedings of the 23rd IEEE International Symposium on Software Reliability Engineering (ISSRE). 2012, 51–60

[184] Letarte D. Conversion of fast inter-procedural static analysis to model checking. In: Proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM). 2010, 1–2

[185] Yang G, Dwyer M B, Rothermel G. Regression model checking. In: Proceedings of the 25th IEEE International Conference on Software Maintenance (ICSM). 2009, 115–124

[186] Sabetzadeh M, Nejati S, Liaskos S, Easterbrook S M, Chechik M. Consistency checking of conceptual models via model merging. In: Proceedings of the 15th IEEE International Requirements Engineering Conference (RE). 2007, 221–230

[187] Fuxman A, Mylopoulos J, Pistore M, Traverso P. Model checking early requirements specifications in tropos. In: Proceedings of the 9th IEEE International Requirements Engineering Conference (RE). 2001, 174–181

[188] Biere A, Cimatti A, Clarke E M, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 1999, 193–207

[189] McMillan K L. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1993

[190] Holzmann G J, Smith M H. A practical method for the verifying event-driven software. In: Proceedings of the 21st International Conference on Software Engineering (ICSE). 1999, 597–607

[191] Holzmann G J, Smith M H. Automating software feature verification. Bell Labs Technical Journal, 2000, 5(2): 72–87

[192] Holzmann G J. Logic verification of ANSI-C code with SPIN. In: Proceedings of the 7th SPIN Workshop. 2000, 131–147

[193] Holzmann G J. From code to models. In: Proceedings of the 2nd International Conference on Application of Concurrency to System Design. 2001, 3–10

[194] Holzmann G J, Smith M H. An automated verification method for distributed systems software based on model extraction. IEEE Transactions on Software Engineering, 2002, 28(4): 364–377

[195] Holzmann G J, Joshi R. Model driven software verification. In: Proceedings of the 11th SPIN Workshop. 2004, 76–91

[196] Wooldridge M, Huget M P, Fisher M, Parsons S. Model checking for multi agent systems: the Mable language and its applications. International Journal on Artificial Intelligence Tools, 2006, 15(2): 195–226

[197] Vortler T, Rulke S, Hofstedt P. Bounded model checking of Contiki applications. In: Proceedings of the 15th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS). 2012, 258–261

[198] Eisler S, Scheidler C, Josko B, Sandmann G, Stroop J. Preliminary results of a case study: model checking for advanced automotive applications. In: Proceedings of International Symposium on Formal Methods (FM). 2005, 533–536

[199] Espada A R, Gallardo M, Salmeron A, Merino P. Using model checking to generate test cases for android applications. In: Proceedings of the 10th MBT. 2015, 7–21

[200] Aceto L, Morichetta A, Tiezzi F. Decision support for mobile cloud computing applications via model checking. In: Proceedings of the 3rd Mobile Cloud. 2015, 199–204

[201] Huang Y W, Yu F, Hang C, Tsai C H, Lee D T, Kuo S Y. Verifying Web applications using bounded model checking. In: Proceedings of IEEE International Conference on Dependable Systems and Networks. 2004, 199–208

[202] Armando A, Carbone R, Compagna L, Li K, Pellegrino G. Model checking driven security testing of web-based applications. In: Proceedings of the 3rd IEEE International Conference on Software Testing, Verification, and Validation Workshops. 2010, 361–370

[203] Li L, Miao H, Chen S. Test generation for web applications usingmodel-checking. In: Proceedings on 11th ACIS International Conference on Software Engineering Artificial Intelligence Networking and Parallel/Distributed Computing. 2010, 237–242

[204] Choi E H, Watanabe H. Model checking class specifications for Web applications. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference. 2005, 67–78

[205] Sciascio E D, Donini F M, Mongiello M, Totaro R, Castelluccia D. Design verification ofWeb applications using symbolic model checking. In: Proceedings of the 5th International Conference on Web Engineering. 2005, 69–74

[206] Nakajima S. Model-checking behavioral specification of BPEL applications. Electronic Notes in Theoretical Computer Science, 2006, 151(2): 19–105

[207] Ghezzi C, Pezze M, Tamburrelli G. Adaptive REST applications viamodel inference and probabilistic model checking. In: Proceedings of IFIP/IEEE International Symposium on Integrated Network Management. 2013, 1376–1382

[208] Gligoric M, Majumdar R. Model checking database applications. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013, 549–564

[209] Cofer D D, Engstrom E, Goldman R P, Musliner D J, Vestal S. Applications of model checking at Honey well Laboratories. In: Proceedings of the 8th SPIN Workshop. 2001, 296–303

[210] Cimatti A. Industrial applications of model checking. In: Proceedings of the 4th MOVEP. 2000, 153–168

[211] Hoque K A, Mohamed O A, Savaria Y, Thibeault C. Early analysis of soft error effects for aerospace applications using probabilistic model checking. In: Proceedings of the 2nd FTSCS Workshop. 2013, 54–70

[212] Hoque K A, Mohamed O A, Savaria Y. Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In: Proceedings the Design, Automation & Test in Europe Conference & Exhibition. 2015, 1635–1640

[213] Armando A, Carbone R, Compagna L. SATMC: a SAT-based model checker for security-critical systems. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2014: 31–45

[214] Loding H. Model-based scenario testing and model checking with applications in the railway domain. Dissertation for the Doctoral Degree, 2014

[215] Azimi S, Gratie C, Ivanov S, Manzoni L, Petre I, Porreca A E. Complexity of model checking for reaction systems. Theoretical Computer Science, 2016, 623: 103–113

[216] Zuliani P. Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 527–536

[217] Clarke E M, Faeder J R, Langmead C J, Harris L A, Jha S K, Legay A. Statistical model checking in biolab: applications to the automated analysis of T-cell receptor signaling pathway. In: Proceedings of International Conference on Computational Methods in Systems Biology. 2008, 231–250

[218] Blackham B, Heiser G. Sequoll: a framework for model checking binaries. In: Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium. 2013, 97–106

[219] Christodorescu M, Jha S. Static analysis of executables to detect malicious patterns. In: Proceedings on 12th USENEX Security Symposium. 2003

[220] Merz S. Model checking: a tutorial overview. In: Cassez F, Jard C, Rozoy B, et al, eds. Modelling and Verification of Parallel Processes. Berlin: Springer-Verlag, 2001, 3–38

[221] Chen J, Zhou H, Bruda S D. Combining model checking and testing for software analysis. In: Proceeding of International Conference on Computer Science and Software Engineering. 2008, 206–209

[222] Steffen B. Data flow analysis as model checking. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 1991, 346–365

[223] Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8), 677–691

[224] Valmari A. A stubborn attack on state explosion. In: Proceedings of the 2nd International Conference on Computer Aided Verification (CAV). 1990, 156–165

[225] Peled D A. All from one, one for all: model checking using representatives. In: Proceedings of the 5th International Conference on Computer Aided Verification (CAV). 1993, 409–423

[226] Godefroid P. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Dissertation for the Doctoral Degree, 1996

[227] Yang Y, Chen X, Gopalakrishnan G, Kirby R M. Distributed dynamic partial order reduction based verification of threaded software. In: Proceedings of the 14th SPIN Workshop. 2007, 58–75

[228] Kahlon V, Wang C, Gupta A. Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Proceedings of the 21st International Conference on Computer Aided Verification (CAV). 2009, 398–413

[229] Tasharofi S, Karmani R K, Lauterburg S, Legay A, Marinov D, Agha G. Trans DPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Proceedings of Formal Techniques for Distributed Systems. 2012, 219–234

[230] Abdulla P A, Aronis S, Jonsson B, Sagonas K F. Optimal dynamic partial order reduction. In: Proceedings of the 41st POPL. 2014, 373–384

[231] Sheeran M, Singh S, Stalmarck G. Checking safety properties using induction and a SAT-solver. In: Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. 2000, 108–125

[232] McMillan K L. Applying SATmethods in unbounded symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV). 2002, 250–264

[233] McMillan K L. Interpolation and SAT-based model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV). 2003, 1–13

[234] Ganai M K, Gupta A, Ashar P.Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of IEEE/ACM International Conference on Computer-aided Design. 2004, 510–517

[235] Gunther H, Weissenbacher G. Incremental bounded software model checking. In: Proceedings of SPIN Workshop, 2014, 40–47

[236] Tinelli C. SMT-based model checking. In: Proceedings of the 4th NASA Formal Methods. 2012

[237] Garcia M, Monteiro F R, Cordeiro L C, Filho E B L. ESBMC: a bounded model checking tool to verify Qt applications. In: Proceedings of the 23rd SPIN Workshop. 2016, 97–103

[238] Hinton A, Kwiatkowska M Z, Norman G, Parker D. PRISM: a tool for automatic verification of probabilistic systems. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2006, 441–444

[239] Hartmanns A, Timmer M. Sound statistical model checking for MDP using partial order and confluence reduction. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 429–456

[240] Jegourel C, Legay A, Sedwards S. Command-based importance sampling for statistical model checking. Theoretical Computer Science, 2016, 649: 1–24

[241] Geldenhuys J. State caching reconsidered. In: Proceedings of the 11th SPIN Workshop. 2004, 23–38

[242] Clarke E M. Counterexample-guided abstraction refinement. In: Proceedings of TIME-ICTL. 2003, 7–8

[243] Rabbi F, Wang H, MacCaull W, Rutle A. A model slicing method for work flow verification. Electronic Notes in Theoretical Computer Science, 2013, 295: 79–93

[244] Self J P, Mercer E G. On-the-Fly dynamic dead variable analysis. In: Proceedings of the 14th SPIN Workshop. 2007, 113–130

[245] Evangelista S. Dynamic delayed duplicate detection for external memory model checking. In: Proceedings of the 15th SPIN Workshop. 2008, 77–94

[246] Chen Z, Motet G. Never trace claims for model checking. In: Proceedings of the 17th SPIN Workshop. 2010, 162–179

[247] Lugiez D, Niebert P, Zennou S. Dynamic bounds and transition merging for local first search. In: Proceedings of the 9th SPIN Workshop. 2002, 221–229

[248] Holzmann G J. State compression in SPIN: recursive indexing and compression training runs. In: Proceedings of the 3rd SPIN Workshop. 1997, 1–10

[249] Nguyen V Y, Ruys T C. Incremental hashing for Spin. In: Proceedings of the 15th SPIN Workshop. 2008, 232–249

[250] Rangarajan M, Dajani-Brown S, Schloegel K, Cofer D D. Analysis of distributed SPIN applied to industrial-scale models. In: Proceedings of the 11th SPIN Workshop. 2004, 267–285

[251] Melatti I, Palmer R, Sawaya G, Yang Y, Kirby R M, Gopalakrishnan G. Parallel and distributed model checking in Eddy. In: Proceedings of the 13th SPIN Workshop. 2006, 108–125

[252] Laster K, Grumberg O. Modular model checking of software. In: Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 1998, 20–35

[253] Brim L, Crhova J, Yorav K. Using assumptions to distribute CTL model checking. Electronic Notes in Theoretical Computer Science, 2002, 68(4): 559–574

[254] Holzmann G J, Bosnacki D. Multi-core model checking with SPIN. In: Proceedings of IEEE International Parallel and Distributed Processing Symposium. 2007, 1–8

[255] Laarman A, Pol J, Weber M. Parallel recursive state compression for free. In: Proceedings of the 18th SPIN Workshop. 2011, 38–56

[256] Ditter A, Ceska M, Luttgen G. On parallel software verification using boolean equation systems. In: Proceedings of the 19th SPIN Workshop. 2012, 80–97

[257] Holzmann G J. Parallelizing the SPIN model checker. In: Proceedings of the 19th SPIN Workshop. 2012, 155–171

[258] Burns E, Zhou R. Parallel model checking using abstraction. In: Proceedings of the 19th SPIN Workshop. 2012, 172–190

[259] Barnat J, Brim L, Simecek P. I/O efficient accepting cycle detection. In: Proceedings of the International Conference on Computer Aided Verification (CAV). 2007, 281–293

[260] Barnat J, Brim L, Simecek P, Weber M. Revisiting resistance speed sup i/o-efficient LTL model checking. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2008, 48–62

[261] Edelkamp S, Sanders P, Simecek P. Semi-external LTL model checking. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV). 2008, 530–542

[262] Wu L, Huang H, Su K, Cai S, Zhang X. An i/o efficient model checking algorithm for large-scale systems. IEEE Transactions on Very Large Scale Integration Systems, 2015, 23(5): 905–915

[263] Ganai M K, Wang C, Li W. Efficient state space exploration: interleaving stateless and state-based model checking. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design (ICCAD). 2010, 786–793

[264] Evangelista S, Kristensen L M. Combining the sweep-line method with the use of an external-memory priority queue. In: Proceedings of the 19th SPIN Workshop. 2012, 43–61

[265] Havelund K. Java Path Finder, a translator from Java to Promela. In: Proceedings of the 6th SPIN Workshop. 1999

[266] Cimatti A, Clarke E M, Giunchiglia F, Roveri M. NUSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2000, 2(4): 410–425

[267] Sun J, Liu Y, Roychoudhury A, Liu S, Dong J S. Fair model checking with process counter abstraction. In: Proceedings of International Symposium on Formal Methods. 2009, 123–139

[268] Klein J, Baier C, Chrszon P, Daum M, Dubslaff C, Kluppelholz S, Marcker S, Muller D. Advances in symbolic probabilistic model checking with PRISM. In: Proceedings of the 22nd nternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2016, 349–366

[269] Godefroid P, Levin M Y, Molnar D A. SAGE: white box fuzzing for security testing. Communications of the ACM, 2012, 55(3): 40–44

[270] Thomas A H, Ranjit J, Rupak M, Gregoire S. Software verification with BLAST. In: Proceedings of the 10th SPIN Workshop. 2003, 235–239

[271] James C K. Symbolic execution and program testing. Communications of the ACM, 1976, 19(7): 385–394

[272] Ciortea L, Zamfir C, Bucur S, Chipounov V, Candea G. Cloud9: a software testing service. ACM SIGOPS Operating Systems Review, 2010, 43(4): 5–10

[273] Karna A K, Du J, Shen H, Zhong H, Gong J, Yu H, Ma X, Zhao J. Tuning parallel symbolic execution engine for better performance. Frontiers of Computer Science. 2018, 12(1): 86–100

[274] Khurshid S, Pasareanu C S, Visser W. Generalized symbolic execution for model checking and testing. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2003, 553–568

[275] Amjad H. Combining model checking and theorem proving. Dissertation for the Doctoral Degree, 2004

[276] Uribe T E. Combinations of model checking and theorem proving. In: Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS). 2000, 151–170

[277] Hungar H. Combining model checking and theorem proving to verify parallel processes. In: Proceedings of the 5th International Conference on Computer Aided Verification (CAV). 1993, 154–165

[278] Dybjer P, Haiyan Q, Takeyama M. Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology, 2004, 46(15): 1011–1025

[279] Amjad H. Verification of AMBA using a combination of model checking and theorem proving. Electronic Notes in Theoretical Computer Science, 2006, 145: 45–61

[280] Seidel P. A case for multi-level combination of theorem proving and model checking tools. In: Proceedings of the 15th MTV Workshop. 2014, 90–97

RIGHTS & PERMISSIONS

2018 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature