Please wait a minute...
Shopping Cart Email List Chinese
Advanced Search Fig/Tab
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Featured Articles  |  Most Downloaded  |  Most Reading
Online Submission Subscribe to Our RSS Content Feed
Front. Comput. Sci.    2018, Vol. 12 Issue (4) : 642-668    https://doi.org/10.1007/s11704-016-6192-0
REVIEW ARTICLE
The role of model checking in software engineering
Anil Kumar KARNA1(), Yuting CHEN1, Haibo YU, Hao ZHONG1, Jianjun ZHAO3
1. Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China
2. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China
3. Department of Advanced Information Technology, Kyushu University, Fukuoka 819-0395, Japan
 Download: PDF(1470 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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     
Corresponding Author(s): Anil Kumar KARNA,Haibo YU   
Just Accepted Date: 26 December 2016   Online First Date: 09 May 2018    Issue Date: 14 June 2018
 Cite this article:   
Anil Kumar KARNA,Yuting CHEN,Haibo YU, et al. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-016-6192-0
https://academic.hep.com.cn/fcs/EN/Y2018/V12/I4/642
1 Ben-Ari M. A primer on model checking. Inroads, 2010, 1(1): 40–47
https://doi.org/10.1145/1721933.1721950
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
https://doi.org/10.1007/978-3-319-07995-0_44
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
https://doi.org/10.1007/s100090050032
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
https://doi.org/10.1016/j.cl.2004.02.006
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
https://doi.org/10.1007/978-3-642-15025-8_13
10 Fraser G, Wotawa F, Ammann P. Testing with model checkers: a survey. Software Testing, Verification & Reliability, 2009, 19(3): 215–261
https://doi.org/10.1002/stvr.402
11 Grumberg O, Veith H. 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 2008
https://doi.org/10.1007/978-3-540-69850-0
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
https://doi.org/10.1007/3-540-11494-7_22
14 Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74–84
https://doi.org/10.1145/1592761.1592781
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
https://doi.org/10.1145/1101908.1101982
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
https://doi.org/10.1145/1858996.1859099
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
https://doi.org/10.1109/ASE.2000.873671
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
https://doi.org/10.1109/ASE.2001.989811
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
https://doi.org/10.1109/ASE.2001.989826
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
https://doi.org/10.1109/ASE.2003.1240299
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
https://doi.org/10.1109/ASE.2011.6100131
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
https://doi.org/10.1109/ASE.2002.1115016
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
https://doi.org/10.1109/ASE.2003.1240300
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
https://doi.org/10.1145/1321631.1321694
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
https://doi.org/10.1109/ASE.2000.873645
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
https://doi.org/10.1109/ASE.2001.989812
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
https://doi.org/10.1109/ASE.2009.82
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
https://doi.org/10.1145/1858996.1859042
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
https://doi.org/10.1109/ASE.2002.1114992
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
https://doi.org/10.1145/1101908.1101989
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
https://doi.org/10.1109/ASE.2001.989825
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
https://doi.org/10.1109/ASE.2008.80
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
https://doi.org/10.1145/1321631.1321719
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
https://doi.org/10.1109/ASE.2011.6100090
39 Crhova J. Distributed modular model checking. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE). 2002, 312
https://doi.org/10.1109/ASE.2002.1115041
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
https://doi.org/10.1109/ASE.2006.10
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
https://doi.org/10.1109/ASE.2011.6100043
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
https://doi.org/10.1109/ASE.2009.43
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
https://doi.org/10.1145/1101908.1101980
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
https://doi.org/10.1109/ASE.2009.32
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
https://doi.org/10.1145/1858996.1859044
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
https://doi.org/10.1109/ASE.2008.29
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
https://doi.org/10.1109/ASE.2008.22
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
https://doi.org/10.1109/ASE.2013.6693074
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
https://doi.org/10.1109/ASE.2009.63
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
https://doi.org/10.1109/ASE.2011.6100143
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
https://doi.org/10.1145/1858996.1859009
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
https://doi.org/10.1109/ASE.2009.16
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
https://doi.org/10.1109/ASE.2006.63
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
https://doi.org/10.1109/ASE.2008.30
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
https://doi.org/10.1145/2351676.2351743
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
https://doi.org/10.1145/1321631.1321691
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
https://doi.org/10.1145/1321631.1321734
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.
https://doi.org/10.1109/ASE.2013.6693138
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
https://doi.org/10.1145/1858996.1859043
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
https://doi.org/10.1145/2970276.2970319
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
https://doi.org/10.1109/ASE.2015.108
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
https://doi.org/10.1109/ICSE.2015.81
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
https://doi.org/10.1109/ICSE.2013.6606566
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
https://doi.org/10.1145/1368088.1368208
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
https://doi.org/10.1109/ICSE.2007.91
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
https://doi.org/10.1145/337180.337219
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
https://doi.org/10.1109/ICSE.2012.6227085
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
https://doi.org/10.1145/1134285.1134409
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
https://doi.org/10.1145/1134285.1134329
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
https://doi.org/10.1145/1810295.1810396
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
https://doi.org/10.1145/1985793.1985839
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
https://doi.org/10.1145/1806799.1806850
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
https://doi.org/10.1145/1985793.1985838
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
https://doi.org/10.1109/ICSE.2015.40
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
https://doi.org/10.1109/ICSE.2012.6227150
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
https://doi.org/10.1109/ICSE.2013.6606593
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
https://doi.org/10.1145/1810295.1810379
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
https://doi.org/10.1145/581339.581393
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
https://doi.org/10.1145/337180.337220
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
https://doi.org/10.1109/ICSE.2001.919196
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
https://doi.org/10.1145/1368088.1368187
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
https://doi.org/10.1109/ICSE.2013.6606751
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
https://doi.org/10.1145/2889160.2891042
92 Han T, Katoen J-P, Damman B. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering, 2009, 35(2): 241–257
https://doi.org/10.1109/TSE.2009.5
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
https://doi.org/10.1109/TSE.2014.2357442
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
https://doi.org/10.1109/TSE.2013.14
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
https://doi.org/10.1109/TSE.2012.41
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
https://doi.org/10.1109/TSE.2013.49
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
https://doi.org/10.1109/TSE.2010.31
98 Santone A. Heuristic search+ local model checking in selective mucalculus. IEEE Transactions on Software Engineering, 2003, 29(6): 510–523
https://doi.org/10.1109/TSE.2003.1205179
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
https://doi.org/10.1109/32.730543
100 Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279–295
https://doi.org/10.1109/32.588521
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
https://doi.org/10.1109/32.926177
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
https://doi.org/10.1109/TSE.2007.70724
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
https://doi.org/10.1109/TSE.2010.68
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
https://doi.org/10.1109/32.708566
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
https://doi.org/10.1109/32.908961
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
https://doi.org/10.1109/TSE.2011.59
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
https://doi.org/10.1109/TSE.2012.44
108 Paolieri M, Horvath A, Vicario E. Probabilistic model checking of regenerative concurrent systems. IEEE Transactions on Software Engineering, 2016, 42(2): 153–169
https://doi.org/10.1109/TSE.2015.2468717
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
https://doi.org/10.1109/TSE.2015.2508444
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
https://doi.org/10.1109/TSE.2015.2488645
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
https://doi.org/10.1007/11823230_5
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
https://doi.org/10.1007/3-540-49727-7_22
113 Podelski A. Model checking as constraint solving. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 22–37
https://doi.org/10.1007/978-3-540-45099-3_2
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
https://doi.org/10.1007/3-540-60360-3_32
115 Saidi H. Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 377–396
https://doi.org/10.1007/978-3-540-45099-3_20
116 Levi F. A symbolic semantics for abstract model checking. In: Proceedings of the 5th International Static Analysis Symposium (SAS). 1998, 134–151
https://doi.org/10.1007/3-540-49727-7_8
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
https://doi.org/10.1007/3-540-45789-5_28
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
https://doi.org/10.1007/3-540-47764-0_20
120 Ranzato F, Tapparo F. Making abstract model checking strongly preserving. In: Proceedings of the 9th International Static Analysis Symposium (SAS). 2002, 411–427
https://doi.org/10.1007/3-540-45789-5_29
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
https://doi.org/10.1007/978-3-642-03237-0_8
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
https://doi.org/10.1007/978-3-662-46675-9_13
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
https://doi.org/10.1007/3-540-36578-8_23
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
https://doi.org/10.1007/3-540-45923-5_24
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
https://doi.org/10.1007/3-540-45923-5_5
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
https://doi.org/10.1007/978-3-540-24721-0_23
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
https://doi.org/10.1007/978-3-540-24721-0_24
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
https://doi.org/10.1007/978-3-540-78743-3_17
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
https://doi.org/10.1007/978-3-642-37057-1_11
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
https://doi.org/10.1007/BFb0053592
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
https://doi.org/10.1007/978-3-642-54804-8_1
132 Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Proceedings of the 11th ESEC/FSE. 2003, 257–266
https://doi.org/10.1145/940071.940106
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
https://doi.org/10.1007/3-540-63531-9_18
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
https://doi.org/10.1145/940071.940097
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
https://doi.org/10.1145/503209.503232
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
https://doi.org/10.1007/3-540-48166-4_10
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
https://doi.org/10.1145/2491411.2491454
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
https://doi.org/10.1145/2491411.2494595
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
https://doi.org/10.1145/1387673.1387678
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
https://doi.org/10.1145/244795.244803
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
https://doi.org/10.1145/262004.262008
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
https://doi.org/10.1145/1011508.1011511
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
https://doi.org/10.1145/325478.325480
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
https://doi.org/10.1145/186025.186051
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
https://doi.org/10.1145/2806886
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
https://doi.org/10.1145/1348250.1348256
149 Krishnamurthi S, Fisler K. Foundations of incremental aspect modelchecking. ACM Transactions on Software Engineering and Methodology, 2007, 16(2): 7
https://doi.org/10.1145/1217295.1217296
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
https://doi.org/10.1145/1243987.1243989
151 Basu S, Smolka S A. Model checking the Java metalocking algorithm. ACM Transactions on Software Engineering and Methodology, 2007, 16(3): 12
https://doi.org/10.1145/1243987.1243990
152 Eshuis R. Symbolic model checking of UML activity diagrams. ACM Transactions on Software Engineering and Methodology, 2006, 15(1): 1–38
https://doi.org/10.1145/1125808.1125809
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
https://doi.org/10.1145/350887.350891
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
https://doi.org/10.1145/990010.990011
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
https://doi.org/10.1145/1146238.1146256
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
https://doi.org/10.1145/2483760.2483779
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
https://doi.org/10.1145/1007512.1007547
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
https://doi.org/10.1145/2771783.2784771
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
https://doi.org/10.1145/271771.271798
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
https://doi.org/10.1145/566172.566175
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
https://doi.org/10.1145/2535838.2535873
162 Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd POPL. 2005, 110–121
https://doi.org/10.1145/1040305.1040315
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
https://doi.org/10.1145/503272.503278
164 Schmidt D A, Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th POPL. 1998, 38–48
https://doi.org/10.1145/268946.268950
165 Godefroid P. Model checking for programming languages using Verisoft. In: Proceedings of the 24th POPL. 1997, 174–186
https://doi.org/10.1145/263699.263717
166 Clarke E M, Grumberg O, Long D E. Model checking and abstraction. In: Proceedings of the 19th POPL. 1992, 342–354
https://doi.org/10.1145/143165.143235
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
https://doi.org/10.1109/TC.2007.1021
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
https://doi.org/10.1109/TC.2009.105
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
https://doi.org/10.1109/TC.2009.187
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
https://doi.org/10.1109/TC.2013.63
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
https://doi.org/10.1145/1869459.1869461
173 Demsky B, Lam P. SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of OOPSLA. 2015, 20–36
https://doi.org/10.1145/2814270.2814297
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
https://doi.org/10.1145/2814270.2814282
175 Darga P T, Boyapati C. Efficient software model checking of data structure properties. In: Proceedings of OOPSLA. 2006, 363–382
https://doi.org/10.1145/1167473.1167504
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
https://doi.org/10.1145/1449764.1449803
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
https://doi.org/10.1145/1250734.1250737
178 Huang J. Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of PLDI. 2015, 165–174
https://doi.org/10.1145/2737924.2737975
179 Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI. 2011, 222–233
https://doi.org/10.1145/1993498.1993525
180 Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of PLDI. 2008, 362–371
https://doi.org/10.1145/1375581.1375625
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
https://doi.org/10.1109/ISSRE.2011.22
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
https://doi.org/10.1109/ISSRE.2012.35
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
https://doi.org/10.1109/ICSM.2010.5609537
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
https://doi.org/10.1109/RE.2007.18
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
https://doi.org/10.21236/ADA360973
189 McMillan K L. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1993
https://doi.org/10.1007/978-1-4615-3190-6
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
https://doi.org/10.1145/302405.302710
191 Holzmann G J, Smith M H. Automating software feature verification. Bell Labs Technical Journal, 2000, 5(2): 72–87
https://doi.org/10.1002/bltj.2223
192 Holzmann G J. Logic verification of ANSI-C code with SPIN. In: Proceedings of the 7th SPIN Workshop. 2000, 131–147
https://doi.org/10.1007/10722468_8
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
https://doi.org/10.1109/CSD.2001.981759
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
https://doi.org/10.1109/TSE.2002.995426
195 Holzmann G J, Joshi R. Model driven software verification. In: Proceedings of the 11th SPIN Workshop. 2004, 76–91
https://doi.org/10.1007/978-3-540-24732-6_6
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
https://doi.org/10.1142/S0218213006002631
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
https://doi.org/10.1109/DDECS.2012.6219069
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
https://doi.org/10.1007/11526841_36
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
https://doi.org/10.4204/EPTCS.180.1
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
https://doi.org/10.1109/MobileCloud.2015.21
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
https://doi.org/10.1109/ICSTW.2010.54
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
https://doi.org/10.1109/APSEC.2005.79
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
https://doi.org/10.1016/j.entcs.2005.07.038
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
https://doi.org/10.1007/978-3-642-36742-7_40
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
https://doi.org/10.7873/DATE.2015.0817
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
https://doi.org/10.1007/978-3-642-54862-8_3
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
https://doi.org/10.1016/j.tcs.2015.11.040
216 Zuliani P. Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 527–536
https://doi.org/10.1007/s10009-014-0343-0
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
https://doi.org/10.1007/978-3-540-88562-7_18
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
https://doi.org/10.1109/RTAS.2013.6531083
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
https://doi.org/10.1007/3-540-45510-8_1
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
https://doi.org/10.1109/CSSE.2008.1025
222 Steffen B. Data flow analysis as model checking. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 1991, 346–365
https://doi.org/10.1007/3-540-54415-1_54
223 Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8), 677–691
https://doi.org/10.1109/TC.1986.1676819
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
https://doi.org/10.1007/3-540-56922-7_34
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
https://doi.org/10.1007/978-3-540-73370-6_6
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
https://doi.org/10.1007/978-3-642-02658-4_31
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
https://doi.org/10.1145/2535838.2535845
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
https://doi.org/10.1007/3-540-40922-X_8
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
https://doi.org/10.1007/3-540-45657-0_19
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
https://doi.org/10.1007/978-3-540-45069-6_1
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
https://doi.org/10.1109/ICCAD.2004.1382631
235 Gunther H, Weissenbacher G. Incremental bounded software model checking. In: Proceedings of SPIN Workshop, 2014, 40–47
https://doi.org/10.1145/2632362.2632374
236 Tinelli C. SMT-based model checking. In: Proceedings of the 4th NASA Formal Methods. 2012
https://doi.org/10.1007/978-3-642-28891-3_1
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
https://doi.org/10.1007/11691372_29
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
https://doi.org/10.1007/s10009-014-0349-7
240 Jegourel C, Legay A, Sedwards S. Command-based importance sampling for statistical model checking. Theoretical Computer Science, 2016, 649: 1–24
https://doi.org/10.1016/j.tcs.2016.08.009
241 Geldenhuys J. State caching reconsidered. In: Proceedings of the 11th SPIN Workshop. 2004, 23–38
https://doi.org/10.1007/978-3-540-24732-6_3
242 Clarke E M. Counterexample-guided abstraction refinement. In: Proceedings of TIME-ICTL. 2003, 7–8
https://doi.org/10.1109/TIME.2003.1214874
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
https://doi.org/10.1016/j.entcs.2013.04.007
244 Self J P, Mercer E G. On-the-Fly dynamic dead variable analysis. In: Proceedings of the 14th SPIN Workshop. 2007, 113–130
https://doi.org/10.1007/978-3-540-73370-6_9
245 Evangelista S. Dynamic delayed duplicate detection for external memory model checking. In: Proceedings of the 15th SPIN Workshop. 2008, 77–94
https://doi.org/10.1007/978-3-540-85114-1_8
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
https://doi.org/10.1007/3-540-46017-9_17
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
https://doi.org/10.1007/978-3-540-85114-1_17
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
https://doi.org/10.1007/978-3-540-24732-6_19
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
https://doi.org/10.1007/11691617_7
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
https://doi.org/10.1007/BFb0054162
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
https://doi.org/10.1016/S1571-0661(05)80758-3
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
https://doi.org/10.1109/IPDPS.2007.370410
255 Laarman A, Pol J, Weber M. Parallel recursive state compression for free. In: Proceedings of the 18th SPIN Workshop. 2011, 38–56
https://doi.org/10.1007/978-3-642-22306-8_4
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
https://doi.org/10.1007/978-3-642-31759-0_8
257 Holzmann G J. Parallelizing the SPIN model checker. In: Proceedings of the 19th SPIN Workshop. 2012, 155–171
https://doi.org/10.1007/978-3-642-31759-0_12
258 Burns E, Zhou R. Parallel model checking using abstraction. In: Proceedings of the 19th SPIN Workshop. 2012, 172–190
https://doi.org/10.1007/978-3-642-31759-0_13
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
https://doi.org/10.1007/978-3-540-73368-3_32
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
https://doi.org/10.1007/978-3-540-70545-1_50
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
https://doi.org/10.1109/TVLSI.2014.2330061
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
https://doi.org/10.1109/ICCAD.2010.5653863
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
https://doi.org/10.1007/978-3-642-31759-0_6
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
https://doi.org/10.1007/s100090050046
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
https://doi.org/10.1007/978-3-642-05089-3_9
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
https://doi.org/10.1007/978-3-662-49674-9_20
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
https://doi.org/10.1145/2093548.2093564
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
https://doi.org/10.1145/360248.360252
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
https://doi.org/10.1145/1713254.1713257
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
https://doi.org/10.1007/s11704-016-5459-9
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
https://doi.org/10.1007/3-540-36577-X_40
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
https://doi.org/10.1007/10720084_11
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
https://doi.org/10.1007/3-540-56922-7_13
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
https://doi.org/10.1016/j.infsof.2004.07.002
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
https://doi.org/10.1016/j.entcs.2005.10.004
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
https://doi.org/10.1109/MTV.2014.29
[1] Ibrahim ALSEADOON, Aakash AHMAD, Adel ALKHALIL, Khalid SULTAN. Migration of existing software systems to mobile computing platforms: a systematic mapping study[J]. Front. Comput. Sci., 2021, 15(2): 152204-.
[2] Zhenghui HU, Wenjun WU, Jie LUO, Xin WANG, Boshu LI. Quality assessment in competition-based software crowdsourcing[J]. Front. Comput. Sci., 2020, 14(6): 146207-.
[3] Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[4] Yixuan TANG, Zhilei REN, Weiqiang KONG, He JIANG. Compiler testing: a systematic literature analysis[J]. Front. Comput. Sci., 2020, 14(1): 1-20.
[5] Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[6] Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[7] Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[8] Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[9] Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[10] Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[11] Wenjun WU, Wei-Tek TSAI, Wei LI. An evaluation framework for software crowdsourcing[J]. Front Comput Sci, 2013, 7(5): 694-709.
[12] Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[13] Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[14] Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[15] Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed