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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ben-Ari M. A primer on model checking. Inroads, 2010, 1(1): 40–47
Baier C, Katoen J-P. Principles of Model Checking. Cambridge: The MIT Press, 2008
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
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
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
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
Bhaduri P, Ramesh S. Model checking of statechart models: survey and research directions. Computer Science, 2004
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
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
Fraser G, Wotawa F, Ammann P. Testing with model checkers: a survey. Software Testing, Verification & Reliability, 2009, 19(3): 215–261
Grumberg O, Veith H. 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 2008
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
Queille J-P, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the International Symposium on Programming. 1982, 337–351
Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74–84
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
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
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
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
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
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
Dwyer M B, Robby, 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
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
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
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
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
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
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
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
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
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
Choi Y, Heimdahl MP 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
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
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
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
Robby, 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
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
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
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
Crhova J. Distributed modular model checking. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE). 2002, 312
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
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
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
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
Haydar M, Boroday S, PetrenkoA, 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
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
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
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
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
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
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
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
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
Vierhauser M, Grunbacher P, EgyedA, 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
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
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
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
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
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
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
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.
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
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
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
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
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
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
Kaveh N. Model checking distributd objects design. In: Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE). 2001, 793–794
Sabetzadeh M, Nejati S, Easterbrook SM, 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
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
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
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
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
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
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
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
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
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
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
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
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
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
Corbett J C, Dwyer M B, Hatcli J, Robby. Bandera: Extracting finitestate models from Java source code. In: Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE). 2000, 439–448
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
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
Alur R, Alfaro L, Grosu R, Henzinger T A, Kang M, Kirsch C M, 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
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
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
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
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
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
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
Han T, Katoen J-P, Damman B. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering, 2009, 35(2): 241–257
Tian C, Duan Z, Duan Z. Making CEGAR more efficient in software model checking. IEEE Transactions on Software Engineering, 2014, 40(12): 1206–1223
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
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
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
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
Santone A. Heuristic search + local model checking in selective mucalculus. IEEE Transactions on Software Engineering, 2003, 29(6): 510–523
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
Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279–295
Bang K-S, Choi J-Y, Yoo C. Comments on “The Model Checker SPIN”. IEEE Transactions on Software Engineering, 2001, 27(6): 573–576
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
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
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
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
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
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
Paolieri M, Horvath A, Vicario E. Probabilistic model checking of regenerative concurrent systems. IEEE Transactions on Software Engineering, 2016, 42(2): 153–169
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
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
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
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
Podelski A. Model checking as constraint solving. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 22–37
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
Saidi H. Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 377–396
Levi F. A symbolic semantics for abstract model checking. In: Proceedings of the 5th International Static Analysis Symposium (SAS). 1998, 134–151
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
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
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
Ranzato F, Tapparo F. Making abstract model checking strongly preserving. In: Proceedings of the 9th International Static Analysis Symposium (SAS). 2002, 411–427
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
Fedyukovich G, D’IddioA 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
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
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
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
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
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
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
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
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
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
Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Proceedings of the 11th ESEC/FSE. 2003, 257–266
Dwyer M B, Carr V, Hines L. Model checking graphical user interfaces using abstractions. In: Proceedings of the 5th ESEC/FSE. 1997, 244–261
Tkachuk O, Dwyer M B. Adapting side effects analysis for modular program model checking. In: Proceedings of the 11th ESEC/FSE. 2003, 188–197
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
Gargantini A, Heitmeyer C L. Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th ESEC/FSE. 1999, 146–162
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
Song F, Touili T. PoMMaDe: pushdown model-checking for mal ware detection. In: Proceedings of the 21st ESEC/FSE. 2013, 607–610
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
Robby, Dwyer MB, Hatcliff J. Bogor: An extensible and highly modular software model checking framework. In: Proceedings of the 11th ESEC/FSE. 2003, 267–276
Naik M, Palsberg J. A type system equivalent to a model checker. ACM Transactions of Programming Languages and Systems, 2008, 30(5): 29
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
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
Sistla A P, Godefroid P. Symmetry and reduced symmetry in model checking. ACM Transactions of Programming Languages and Systems, 2004, 26(4): 702–734
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
Clarke EM, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions of Programming Languages and Systems, 1994, 16(5): 1512–1542
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
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
Krishnamurthi S, Fisler K. Foundations of incremental aspect modelchecking. ACM Transactions on Software Engineering and Methodology, 2007, 16(2): 7
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
Basu S, Smolka S A. Model checking the Java metalocking algorithm. ACM Transactions on Software Engineering and Methodology, 2007, 16(3): 12
Eshuis R. Symbolic model checking of UML activity diagrams. ACM Transactions on Software Engineering and Methodology, 2006, 15(1): 1–38
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
Chechik M, Devereux B, Easterbrook SM, Gurfinkel A. Multi-valued symbolic model-checking. ACM Transactions on Software Engineering and Methodology, 2003, 12(4): 371–408
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
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
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
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
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
Groce A, Visser W. Model checking Java programs using structural heuristics. In: Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA). 2002, 12–21
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
Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd POPL. 2005, 110–121
Chaki S, Rajamani S K, Rehof J. Types as models: model checking message-passing programs. In: Proceedings of the 29th POPL. 2002, 45–57
Schmidt D A, Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th POPL. 1998, 38–48
Godefroid P. Model checking for programming languages using Verisoft. In: Proceedings of the 24th POPL. 1997, 174–186
Clarke EM, Grumberg O, Long D E. Model checking and abstraction. In: Proceedings of the 19th POPL. 1992, 342–354
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
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
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
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
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
Roberson M, Boyapati C. Efficient modular glass box software model checking. In: Proceedings of OOPSLA. 2010, 4–21
Demsky B, Lam P. SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of OOPSLA. 2015, 20–36
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
Darga P T, Boyapati C. Efficient software model checking of data structure properties. In: Proceedings of OOPSLA. 2006, 363–382
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
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
Huang J. Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of PLDI. 2015, 165–174
Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI. 2011, 222–233
Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of PLDI. 2008, 362–371
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
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
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
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
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
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
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
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
McMillan K L. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1993
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
Holzmann G J, Smith M H. Automating software feature verification. Bell Labs Technical Journal, 2000, 5(2): 72–87
Holzmann G J. Logic verification of ANSI-C code with SPIN. In: Proceedings of the 7th SPIN Workshop. 2000, 131–147
Holzmann G J. From code to models. In: Proceedings of the 2nd International Conference on Application of Concurrency to System Design. 2001, 3–10
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
Holzmann G J, Joshi R. Model driven software verification. In: Proceedings of the 11th SPIN Workshop. 2004, 76–91
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
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
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
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
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
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
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
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
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
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
Nakajima S. Model-checking behavioral specification of BPEL applications. Electronic Notes in Theoretical Computer Science, 2006, 151(2): 19–105
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
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
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
Cimatti A. Industrial applications of model checking. In: Proceedings of the 4th MOVEP. 2000, 153–168
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
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
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
Loding H. Model-based scenario testing and model checking with applications in the railway domain. Dissertation for the Doctoral Degree, 2014
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
Zuliani P. Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 527–536
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
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
Christodorescu M, Jha S. Static analysis of executables to detect malicious patterns. In: Proceedings on 12th USENEX Security Symposium. 2003
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
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
Steffen B. Data flow analysis as model checking. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 1991, 346–365
Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8), 677–691
Valmari A. A stubborn attack on state explosion. In: Proceedings of the 2nd International Conference on Computer Aided Verification (CAV). 1990, 156–165
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
Godefroid P. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Dissertation for the Doctoral Degree, 1996
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
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
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
Abdulla P A, Aronis S, Jonsson B, Sagonas K F. Optimal dynamic partial order reduction. In: Proceedings of the 41st POPL. 2014, 373–384
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
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
McMillan K L. Interpolation and SAT-based model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV). 2003, 1–13
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
Gunther H, Weissenbacher G. Incremental bounded software model checking. In: Proceedings of SPIN Workshop, 2014, 40–47
Tinelli C. SMT-based model checking. In: Proceedings of the 4th NASA Formal Methods. 2012
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
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
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
Jegourel C, Legay A, Sedwards S. Command-based importance sampling for statistical model checking. Theoretical Computer Science, 2016, 649: 1–24
Geldenhuys J. State caching reconsidered. In: Proceedings of the 11th SPIN Workshop. 2004, 23–38
Clarke E M. Counterexample-guided abstraction refinement. In: Proceedings of TIME-ICTL. 2003, 7–8
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
Self J P, Mercer E G. On-the-Fly dynamic dead variable analysis. In: Proceedings of the 14th SPIN Workshop. 2007, 113–130
Evangelista S. Dynamic delayed duplicate detection for external memory model checking. In: Proceedings of the 15th SPIN Workshop. 2008, 77–94
Chen Z, Motet G. Never trace claims for model checking. In: Proceedings of the 17th SPIN Workshop. 2010, 162–179
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
Holzmann G J. State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of the 3rd SPIN Workshop. 1997, 1–10
Nguyen V Y, Ruys T C. Incremental hashing for Spin. In: Proceedings of the 15th SPIN Workshop. 2008, 232–249
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
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
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
Brim L, Crhova J, Yorav K. Using assumptions to distribute CTL model checking. Electronic Notes in Theoretical Computer Science, 2002, 68(4): 559–574
Holzmann G J, Bosnacki D. Multi-core model checking with SPIN. In: Proceedings of IEEE International Parallel and Distributed Processing Symposium. 2007, 1–8
Laarman A, Pol J, Weber M. Parallel recursive state compression for free. In: Proceedings of the 18th SPIN Workshop. 2011, 38–56
Ditter A, Ceska M, Luttgen G. On parallel software verification using boolean equation systems. In: Proceedings of the 19th SPIN Workshop. 2012, 80–97
Holzmann G J. Parallelizing the SPIN model checker. In: Proceedings of the 19th SPIN Workshop. 2012, 155–171
Burns E, Zhou R. Parallel model checking using abstraction. In: Proceedings of the 19th SPIN Workshop. 2012, 172–190
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
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
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
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
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
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
Havelund K. Java Path Finder, a translator from Java to Promela. In: Proceedings of the 6th SPIN Workshop. 1999
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
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
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
Godefroid P, Levin M Y, Molnar D A. SAGE: white box fuzzing for security testing. Communications of the ACM, 2012, 55(3): 40–44
Thomas A H, Ranjit J, Rupak M, Gregoire S. Software verification with BLAST. In: Proceedings of the 10th SPIN Workshop. 2003, 235–239
James C K. Symbolic execution and program testing. Communications of the ACM, 1976, 19(7): 385–394
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
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
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
Amjad H. Combining model checking and theorem proving. Dissertation for the Doctoral Degree, 2004
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
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
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
Amjad H. Verification of AMBA using a combination of model checking and theorem proving. Electronic Notes in Theoretical Computer Science, 2006, 145: 45–61
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
Acknowledgements
The authors are grateful to anonymous referee for their valuable comments and suggestions to improve the presentation and contents of this paper. This research was sponsored in part by the National Basic Research Program of China (2015CB352203) and the National Nature Science Foundation of China (Grant Nos. 61572312 and 61572313). Jianjun Zhao was supported in part by Japan Society for the Promotion of Science, Grantin- Aid for Research Activity Start-up (16H07031). Hao Zhong was partially supported by Science and Technology Commission of Shanghai Municipality’s Innovation Action Plan (15DZ1100305).
Author information
Authors and Affiliations
Corresponding author
Additional information
Anil Kumar Karna received his BE degree in computer science from Huazhong University of Science and Technology, China in 2004, and his MS degree in software engineering from Shanghai Jiao Tong University (SJTU), China in 2010. He worked as web-master, lead IT support engineer, and IT instructor in Nepal, India, and China, respectively from 2004 to 2007. He joined STAP lab as a PhD candidate in the Department of Computer Science and Engineering at SJTU.His current research interests include software reliability, system crashes, program analysis, testing & debugging, and verification & validation.
Yuting Chen received the BS and MS degrees in computer science from Nanjing University, China in 2000 and 2003, respectively. He received the PhD degree in computer science from Hosei University, Japan in 2007. Yuting Chen is now an associate professor at the Computer Science Department of Shanghai Jiao Tong University, China. Chen’s research interests include program analysis, software testing, verification, and validation.
Haibo Yu received her BS degree in computer science from Tsinghua University, China in 1987. She received her MS and PhD degrees in computer science from Kyushu University, Japan in 1999 and 2009, respectively. She joined the School of Software at Shanghai Jiao Tong University, China in March, 2010. Her research interests include software engineering, information retrieval and web application systems.
Hao Zhong received his BS degree from Civil Aviation University of China, China in 2002; and both his MS and PhD degrees from Peking University, China in 2005 and 2009, respectively. After graduation, he worked as an assistant professor at Institute of Software, Chinese Academy of Sciences, China, and was promoted as an associate professor in 2012. From 2013 to 2014, he was a visiting scholar at University of California, Davis. Since 2014, he has become an associate professor at Shanghai Jiao Tong University, China. He is a member of the IEEE and ACM. His research interest is in the area of software engineering, with an emphasis on mining software repositories.
Jianjun Zhao received the BS degree in computer science from Tsinghua University, China in 1987, and the PhD degree in computer science from Kyushu University, Japan in 1997. He is now a professor in the Department of Advanced Information Technology, Kyushu University, Japan. Before joining the faculty in April 2016, he was a professor in the School of Software and also the Department of Computer Science and Engineering from November 2005 to March 2016, at Shanghai Jiao Tong University, China. His research interests include software engineering and programming language, especially program analysis, software testing, code searching and automatic programming.
Electronic supplementary material
Rights and permissions
About this article
Cite this article
Karna, A.K., Chen, Y., Yu, H. et al. The role of model checking in software engineering. Front. Comput. Sci. 12, 642–668 (2018). https://doi.org/10.1007/s11704-016-6192-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11704-016-6192-0