{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T21:27:21Z","timestamp":1790717241033,"version":"4.1.0"},"reference-count":280,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,4,27]],"date-time":"2018-04-27T00:00:00Z","timestamp":1524787200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s11704-016-6192-0","type":"journal-article","created":{"date-parts":[[2018,4,27]],"date-time":"2018-04-27T10:42:33Z","timestamp":1524825753000},"page":"642-668","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["The role of model checking in software engineering"],"prefix":"10.1007","volume":"12","author":[{"given":"Anil Kumar","family":"Karna","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuting","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Haibo","family":"Yu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hao","family":"Zhong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianjun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,27]]},"reference":[{"issue":"1","key":"6192_CR1","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1721933.1721950","volume":"1","author":"M Ben-Ari","year":"2010","unstructured":"Ben-Ari M. A primer on model checking. Inroads, 2010, 1(1): 40\u201347","journal-title":"Inroads"},{"key":"6192_CR2","volume-title":"Cambridge: The MIT Press","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P. Principles of Model Checking. Cambridge: The MIT Press, 2008"},{"key":"6192_CR3","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-319-07995-0_44","volume-title":"Proceeding of International Joint Conference SOCO, CISIS & ICEUTE.","author":"I Garcia-Ferreira","year":"2014","unstructured":"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\u2013452"},{"issue":"3","key":"6192_CR4","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/s100090050032","volume":"2","author":"H R Andersen","year":"1999","unstructured":"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\u2013259","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6192_CR5","first-page":"35","volume-title":"Proceedings of the 15th International Conference on Concurrency Theory.","author":"P A Abdulla","year":"2004","unstructured":"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\u201348"},{"key":"6192_CR6","first-page":"65","volume-title":"Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence.","author":"S Edelkamp","year":"2008","unstructured":"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\u201389"},{"key":"6192_CR7","volume-title":"Computer Science","author":"P Bhaduri","year":"2004","unstructured":"Bhaduri P, Ramesh S. Model checking of statechart models: survey and research directions. Computer Science, 2004"},{"issue":"3\u20134","key":"6192_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.cl.2004.02.006","volume":"30","author":"L D Zuck","year":"2004","unstructured":"Zuck L D, Pnueli A. Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures, 2004, 30(3\u20134): 139\u2013169","journal-title":"Computer Languages, Systems & Structures"},{"key":"6192_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-15025-8_13","volume-title":"Fields of Logic and Computation","author":"T Eiter","year":"2010","unstructured":"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\u2013250"},{"issue":"3","key":"6192_CR10","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2009","unstructured":"Fraser G, Wotawa F, Ammann P. Testing with model checkers: a survey. Software Testing, Verification & Reliability, 2009, 19(3): 215\u2013261","journal-title":"Software Testing, Verification & Reliability"},{"key":"6192_CR11","volume-title":"Berlin: Springer","author":"O Grumberg","year":"2008","unstructured":"Grumberg O, Veith H. 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 2008"},{"key":"6192_CR12","first-page":"52","volume-title":"Proceedings of Workshop on Logic of Programs.","author":"E M Clarke","year":"1981","unstructured":"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\u201371"},{"key":"6192_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the International Symposium on Programming.","author":"J-P Queille","year":"1982","unstructured":"Queille J-P, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the International Symposium on Programming. 1982, 337\u2013351"},{"issue":"11","key":"6192_CR14","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"E M Clarke","year":"2009","unstructured":"Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74\u201384","journal-title":"Communications of the ACM"},{"key":"6192_CR15","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1101908.1101982","volume-title":"Proceedings of the 20th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"N Rungta","year":"2005","unstructured":"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\u2013413"},{"key":"6192_CR16","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1145\/1858996.1859099","volume-title":"Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"D Letarte","year":"2010","unstructured":"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\u2013516"},{"key":"6192_CR17","first-page":"253","volume-title":"Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE).","author":"D Y W Park","year":"2000","unstructured":"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\u2013256"},{"key":"6192_CR18","first-page":"254","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE).","author":"R Iosif","year":"2001","unstructured":"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\u2013261"},{"key":"6192_CR19","first-page":"346","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE).","author":"P Inverardi","year":"2001","unstructured":"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\u2013349"},{"key":"6192_CR20","first-page":"106","volume-title":"Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE).","author":"J Barnat","year":"2003","unstructured":"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\u2013115"},{"key":"6192_CR21","first-page":"154","volume-title":"Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE).","author":"M B R Dwyer","year":"2004","unstructured":"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\u2013163"},{"key":"6192_CR22","first-page":"584","volume-title":"Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"P C Mehlitz","year":"2011","unstructured":"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\u2013587"},{"key":"6192_CR23","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1109\/ASE.2002.1115016","volume-title":"Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE).","author":"K Loer","year":"2002","unstructured":"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\u2013226"},{"key":"6192_CR24","first-page":"116","volume-title":"Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE).","author":"O Tkachuk","year":"2003","unstructured":"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\u2013129"},{"key":"6192_CR25","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1145\/1321631.1321694","volume-title":"Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"O Tkachuk","year":"2007","unstructured":"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\u2013404"},{"key":"6192_CR26","first-page":"3","volume-title":"Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE).","author":"W Visser","year":"2000","unstructured":"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\u201312"},{"key":"6192_CR27","first-page":"262","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE).","author":"G P Brat","year":"2001","unstructured":"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"},{"key":"6192_CR28","first-page":"495","volume-title":"Proceedings of IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"K Kim","year":"2009","unstructured":"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\u2013499"},{"key":"6192_CR29","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/1858996.1859042","volume-title":"Proceedings of the 25th IEEE International Conference on Automated Software Engineering (ASE).","author":"K Kim","year":"2010","unstructured":"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\u2013224"},{"key":"6192_CR30","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/ASE.2002.1114992","volume-title":"Proceedings of the 17th IEEE International Conference on Automated Software Engineering.","author":"M P E Heimdahl","year":"2002","unstructured":"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\u201346"},{"key":"6192_CR31","first-page":"314","volume-title":"Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE).","author":"Y Choi","year":"2003","unstructured":"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\u2013317"},{"key":"6192_CR32","first-page":"333","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE).","author":"F Xie","year":"2001","unstructured":"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\u2013336"},{"key":"6192_CR33","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/1101908.1101989","volume-title":"Proceedings of the 20th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"J Simmonds","year":"2005","unstructured":"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\u2013432"},{"key":"6192_CR34","first-page":"341","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE).","author":"K S Barber","year":"2001","unstructured":"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\u2013345"},{"key":"6192_CR35","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1109\/ASE.2006.34","volume-title":"Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"Robby","year":"2006","unstructured":"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\u2013370"},{"key":"6192_CR36","first-page":"479","volume-title":"Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"T E Hart","year":"2008","unstructured":"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\u2013480"},{"key":"6192_CR37","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1145\/1321631.1321719","volume-title":"Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"T Witkowski","year":"2007","unstructured":"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\u2013504"},{"key":"6192_CR38","first-page":"428","volume-title":"Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"A Vakili","year":"2011","unstructured":"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\u2013431"},{"key":"6192_CR39","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1109\/ASE.2002.1115041","volume-title":"Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE).","author":"J Crhova","year":"2002","unstructured":"Crhova J. Distributed modular model checking. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE). 2002, 312"},{"key":"6192_CR40","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1109\/ASE.2006.10","volume-title":"Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"C Artho","year":"2006","unstructured":"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\u2013188"},{"key":"6192_CR41","first-page":"103","volume-title":"Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"W Leungwattanakit","year":"2011","unstructured":"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\u2013112"},{"key":"6192_CR42","first-page":"447","volume-title":"Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"C Artho","year":"2009","unstructured":"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\u2013458"},{"key":"6192_CR43","first-page":"169","volume-title":"Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"C Artho","year":"2013","unstructured":"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\u2013179"},{"key":"6192_CR44","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1145\/1101908.1101980","volume-title":"Proceedings of the 20th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"M Haydar","year":"2005","unstructured":"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\u2013404"},{"key":"6192_CR45","first-page":"635","volume-title":"Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"J Barnat","year":"2009","unstructured":"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\u2013639"},{"key":"6192_CR46","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/1858996.1859044","volume-title":"Proceedings of the 25th IEEE\/ACMInternational Conference on Automated Software Engineering (ASE).","author":"S Halle","year":"2010","unstructured":"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\u2013244"},{"key":"6192_CR47","first-page":"354","volume-title":"Proceedings of the 19th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"Y Choi","year":"2004","unstructured":"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\u2013357"},{"key":"6192_CR48","first-page":"188","volume-title":"Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"H Post","year":"2008","unstructured":"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\u2013197"},{"key":"6192_CR49","first-page":"119","volume-title":"Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"M Pradella","year":"2008","unstructured":"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\u2013127"},{"key":"6192_CR50","first-page":"136","volume-title":"Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"C Y Cho","year":"2013","unstructured":"Cho C Y, D\u2019Silva 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\u2013146"},{"key":"6192_CR51","first-page":"137","volume-title":"Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"L C Cordeiro","year":"2009","unstructured":"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\u2013148"},{"key":"6192_CR52","first-page":"633","volume-title":"Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"T K Nguyen","year":"2011","unstructured":"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\u2013636"},{"key":"6192_CR53","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1858996.1859009","volume-title":"Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"M Vierhauser","year":"2010","unstructured":"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\u201372"},{"key":"6192_CR54","first-page":"269","volume-title":"Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"K Lauenroth","year":"2009","unstructured":"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\u2013280"},{"key":"6192_CR55","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1109\/ASE.2006.63","volume-title":"Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"C Liu","year":"2006","unstructured":"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\u2013304"},{"key":"6192_CR56","first-page":"198","volume-title":"Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"M Kim","year":"2008","unstructured":"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\u2013207"},{"key":"6192_CR57","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/2351676.2351743","volume-title":"Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"F Song","year":"2012","unstructured":"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\u2013349"},{"key":"6192_CR58","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1145\/1321631.1321691","volume-title":"Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"K Ku","year":"2007","unstructured":"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\u2013392"},{"key":"6192_CR59","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1145\/1321631.1321734","volume-title":"Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"A Armando","year":"2007","unstructured":"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\u2013542"},{"key":"6192_CR60","first-page":"706","volume-title":"Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"S Falke","year":"2013","unstructured":"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\u2013709."},{"key":"6192_CR61","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/1858996.1859043","volume-title":"Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"R He","year":"2010","unstructured":"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\u2013234"},{"key":"6192_CR62","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/2970276.2970319","volume-title":"Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"M Nishi","year":"2016","unstructured":"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\u2013565"},{"key":"6192_CR63","first-page":"807","volume-title":"Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE).","author":"O Inverso","year":"2015","unstructured":"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\u2013812"},{"key":"6192_CR64","first-page":"232","volume-title":"Proceedings of the 25th IEEE International Conference on Software Engineering (ICSE).","author":"H S Hong","year":"2003","unstructured":"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\u2013243"},{"key":"6192_CR65","first-page":"654","volume-title":"Proceedings of the 37th IEEE International Conference on Software Engineering (ICSE).","author":"T Su","year":"2015","unstructured":"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\u2013665"},{"key":"6192_CR66","first-page":"202","volume-title":"Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE).","author":"C Tian","year":"2013","unstructured":"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\u2013211"},{"key":"6192_CR67","first-page":"793","volume-title":"Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE).","author":"N Kaveh","year":"2001","unstructured":"Kaveh N. Model checking distributd objects design. In: Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE). 2001, 793\u2013794"},{"key":"6192_CR68","first-page":"815","volume-title":"Proceedings of the 30th IEEE International Conference on Software Engineering (ICSE).","author":"M Sabetzadeh","year":"2008","unstructured":"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\u2013818"},{"key":"6192_CR69","first-page":"793","volume-title":"Proceedings of the 29th IEEE International Conference on Software Engineering (ICSE).","author":"A Egyed","year":"2007","unstructured":"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\u2013796"},{"key":"6192_CR70","first-page":"335","volume-title":"Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE).","author":"T Bultan","year":"2000","unstructured":"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\u2013344"},{"key":"6192_CR71","first-page":"1337","volume-title":"Proceedings of the 34th IEEE International Conference on Software Engineering (ICSE).","author":"S Song","year":"2012","unstructured":"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\u20131340"},{"key":"6192_CR72","doi-asserted-by":"crossref","first-page":"775","DOI":"10.1145\/1134285.1134409","volume-title":"Proceedings of the 28th IEEE International Conference on Software Engineering (ICSE).","author":"J S Dong","year":"2006","unstructured":"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\u2013778"},{"key":"6192_CR73","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/1134285.1134329","volume-title":"Proceedings of the 28th IEEE International Conference on Software Engineering (ICSE).","author":"F S-H Chang","year":"2006","unstructured":"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\u2013320"},{"key":"6192_CR74","first-page":"373","volume-title":"Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE).","author":"L C Cordeiro","year":"2010","unstructured":"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\u2013376"},{"key":"6192_CR75","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/1985793.1985839","volume-title":"Proceedings of the 33rd IEEE International Conference on Software Engineering (ICSE).","author":"L C Cordeiro","year":"2011","unstructured":"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\u2013340"},{"key":"6192_CR76","first-page":"335","volume-title":"Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE).","author":"A Classen","year":"2010","unstructured":"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\u2013344"},{"key":"6192_CR77","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/1985793.1985838","volume-title":"Proceedings of the 33rd IEEE International Conference on Software Engineering (ICSE).","author":"A Classen","year":"2011","unstructured":"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\u2013330"},{"key":"6192_CR78","first-page":"189","volume-title":"Proceedings of the 37th IEEE International Conference on Software Engineering (ICSE).","author":"S Ben-David","year":"2015","unstructured":"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\u2013199"},{"key":"6192_CR79","first-page":"672","volume-title":"Proceedings of the 34th IEEE International Conference on Software Engineering (ICSE).","author":"M Cordy","year":"2012","unstructured":"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\u2013682"},{"key":"6192_CR80","first-page":"472","volume-title":"Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE).","author":"M Cordy","year":"2013","unstructured":"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\u2013481"},{"key":"6192_CR81","first-page":"333","volume-title":"Proceedings of the 32nd IEEE International Conference on Software Engineering (ICSE).","author":"F G Marinho","year":"2010","unstructured":"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\u2013334"},{"key":"6192_CR82","first-page":"439","volume-title":"Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE).","author":"J C Corbett","year":"2000","unstructured":"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\u2013448"},{"key":"6192_CR83","first-page":"431","volume-title":"Proceedings of the 24th IEEE International Conference on Software Engineering (ICSE).","author":"S Chandra","year":"2002","unstructured":"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\u2013441"},{"key":"6192_CR84","first-page":"345","volume-title":"Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE).","author":"Z Dang","year":"2000","unstructured":"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\u2013354"},{"key":"6192_CR85","first-page":"835","volume-title":"Proceedings of the 23rd IEEE International Conference on Software Engineering (ICSE).","author":"R Alur","year":"2001","unstructured":"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\u2013836"},{"key":"6192_CR86","first-page":"804","volume-title":"Proceedings of the 25th IEEE International Conference on Software Engineering (ICSE).","author":"S M Easterbrook","year":"2003","unstructured":"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\u2013805"},{"key":"6192_CR87","first-page":"693","volume-title":"Proceedings of the 30th IEEE International Conference on Software Engineering (ICSE).","author":"B Long","year":"2008","unstructured":"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\u2013702"},{"key":"6192_CR88","first-page":"1481","volume-title":"Proceedings of the 35th IEEE International Conference on Software Engineering (ICSE).","author":"J S Dong","year":"2013","unstructured":"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\u20131483"},{"key":"6192_CR89","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1145\/302405.302460","volume-title":"Proceedings of the 21st IEEE International Conference on Software Engineering (ICSE).","author":"W Chan","year":"1999","unstructured":"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\u2013151"},{"key":"6192_CR90","first-page":"73","volume-title":"Proceedings of the 38th IEEE International Conference on Software Engineering (ICSE).","author":"G Su","year":"2016","unstructured":"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\u201384"},{"key":"6192_CR91","first-page":"686","volume-title":"Proceedings of the 38th IEEE International Conference on Software Engineering (ICSE).","author":"A Huang","year":"2016","unstructured":"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\u2013688"},{"issue":"2","key":"6192_CR92","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T Han","year":"2009","unstructured":"Han T, Katoen J-P, Damman B. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering, 2009, 35(2): 241\u2013257","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"12","key":"6192_CR93","doi-asserted-by":"publisher","first-page":"1206","DOI":"10.1109\/TSE.2014.2357442","volume":"40","author":"C Tian","year":"2014","unstructured":"Tian C, Duan Z, Duan Z. Making CEGAR more efficient in software model checking. IEEE Transactions on Software Engineering, 2014, 40(12): 1206\u20131223","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"9","key":"6192_CR94","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1109\/TSE.2013.14","volume":"39","author":"Y Moffett","year":"2013","unstructured":"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\u20131325","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"6192_CR95","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1109\/TSE.2012.41","volume":"39","author":"D Alrajeh","year":"2013","unstructured":"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\u2013383","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"5","key":"6192_CR96","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1109\/TSE.2013.49","volume":"40","author":"W Leungwattanakit","year":"2014","unstructured":"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\u2013501","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6192_CR97","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1109\/TSE.2010.31","volume":"36","author":"S Artzi","year":"2010","unstructured":"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\u2013494","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"6","key":"6192_CR98","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1109\/TSE.2003.1205179","volume":"29","author":"A Santone","year":"2003","unstructured":"Santone A. Heuristic search + local model checking in selective mucalculus. IEEE Transactions on Software Engineering, 2003, 29(6): 510\u2013523","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"11","key":"6192_CR99","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C L Heitmeyer","year":"1998","unstructured":"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\u2013948","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"5","key":"6192_CR100","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G J Holzmann","year":"1997","unstructured":"Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279\u2013295","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"6","key":"6192_CR101","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1109\/32.926177","volume":"27","author":"K-S Bang","year":"2001","unstructured":"Bang K-S, Choi J-Y, Yoo C. Comments on \u201cThe Model Checker SPIN\u201d. IEEE Transactions on Software Engineering, 2001, 27(6): 573\u2013576","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"10","key":"6192_CR102","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G J Holzmann","year":"2007","unstructured":"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\u2013674","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"6192_CR103","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/TSE.2010.68","volume":"37","author":"M Kim","year":"2011","unstructured":"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\u2013160","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"7","key":"6192_CR104","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W Chan","year":"1998","unstructured":"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\u2013520","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"6192_CR105","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/32.908961","volume":"27","author":"W Chan","year":"2001","unstructured":"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\u2013190","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6192_CR106","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L C Cordeiro","year":"2012","unstructured":"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\u2013974","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6192_CR107","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1109\/TSE.2012.44","volume":"39","author":"S Ikeda","year":"2013","unstructured":"Ikeda S, Jibiki M, Kuno Y. Coverage estimation in model checking with bits tate hashing. IEEE Transactions on Software Engineering, 2013, 39(4): 477\u2013486","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"6192_CR108","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1109\/TSE.2015.2468717","volume":"42","author":"M Paolieri","year":"2016","unstructured":"Paolieri M, Horvath A, Vicario E. Probabilistic model checking of regenerative concurrent systems. IEEE Transactions on Software Engineering, 2016, 42(2): 153\u2013169","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"7","key":"6192_CR109","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1109\/TSE.2015.2508444","volume":"42","author":"G Su","year":"2016","unstructured":"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\u2013639","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6192_CR110","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1109\/TSE.2015.2488645","volume":"42","author":"H M Chavez","year":"2016","unstructured":"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\u2013344","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6192_CR111","first-page":"52","volume-title":"Proceedings of the 13th International Static Analysis Symposium (SAS).","author":"A Bouajjani","year":"2006","unstructured":"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\u201370"},{"key":"6192_CR112","first-page":"351","volume-title":"Proceedings of the 5th International Static Analysis Symposium (SAS).","author":"D A Schmidt","year":"1998","unstructured":"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\u2013380"},{"key":"6192_CR113","first-page":"22","volume-title":"Proceedings of the 7th International Static Analysis Symposium (SAS).","author":"A Podelski","year":"2000","unstructured":"Podelski A. Model checking as constraint solving. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 22\u201337"},{"key":"6192_CR114","first-page":"51","volume-title":"Proceedings of the 2nd International Static Analysis Symposium (SAS).","author":"R Cleaveland","year":"1995","unstructured":"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\u201363"},{"key":"6192_CR115","first-page":"377","volume-title":"Proceedings of the 7th International Static Analysis Symposium (SAS).","author":"H Saidi","year":"2000","unstructured":"Saidi H. Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (SAS). 2000, 377\u2013396"},{"key":"6192_CR116","first-page":"134","volume-title":"Proceedings of the 5th International Static Analysis Symposium (SAS).","author":"F Levi","year":"1998","unstructured":"Levi F. A symbolic semantics for abstract model checking. In: Proceedings of the 5th International Static Analysis Symposium (SAS). 1998, 134\u2013151"},{"key":"6192_CR117","first-page":"395","volume-title":"Proceedings of the 9th International Static Analysis Symposium (SAS).","author":"M Gallardo","year":"2002","unstructured":"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\u2013410"},{"key":"6192_CR118","first-page":"369","volume-title":"Proceedings of the 18th International Static Analysis Symposium (SAS).","author":"D Monniaux","year":"2011","unstructured":"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\u2013385"},{"key":"6192_CR119","first-page":"356","volume-title":"Proceedings of the 8th International Static Analysis Symposium (SAS).","author":"R Giacobazzi","year":"2001","unstructured":"Giacobazzi R, Quintarelli E. Incompleteness, counterexamples, and refinements in abstract model-checking. In: Proceedings of the 8th International Static Analysis Symposium (SAS). 2001, 356\u2013373"},{"key":"6192_CR120","first-page":"411","volume-title":"Proceedings of the 9th International Static Analysis Symposium (SAS).","author":"F Ranzato","year":"2002","unstructured":"Ranzato F, Tapparo F. Making abstract model checking strongly preserving. In: Proceedings of the 9th International Static Analysis Symposium (SAS). 2002, 411\u2013427"},{"key":"6192_CR121","first-page":"86","volume-title":"Proceedings of the 16th International Static Analysis Symposium (SAS).","author":"M Wehrle","year":"2009","unstructured":"Wehrle M, Helmert M. The causal graph revisited for directed model checking. In: Proceedings of the 16th International Static Analysis Symposium (SAS). 2009, 86\u2013101"},{"key":"6192_CR122","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-662-46675-9_13","volume-title":"Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich G, D\u2019IddioA 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\u2013201"},{"key":"6192_CR123","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-36578-8_23","volume-title":"Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering (FASE)","author":"N Sharygina","year":"2003","unstructured":"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\u2013340"},{"key":"6192_CR124","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45923-5_24","volume-title":"Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"F Xie","year":"2002","unstructured":"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\u2013335"},{"key":"6192_CR125","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-45923-5_5","volume-title":"Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"F Xie","year":"2002","unstructured":"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\u201379"},{"key":"6192_CR126","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-540-24721-0_23","volume-title":"Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"P Saffrey","year":"2004","unstructured":"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\u2013323"},{"key":"6192_CR127","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-540-24721-0_24","volume-title":"Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"F Xie","year":"2004","unstructured":"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\u2013338"},{"key":"6192_CR128","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-78743-3_17","volume-title":"Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"A Fantechi","year":"2008","unstructured":"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\u2013245"},{"key":"6192_CR129","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"D Beyer","year":"2013","unstructured":"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\u2013162"},{"key":"6192_CR130","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/BFb0053592","volume-title":"Proceedings of the 1st International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"A Mota","year":"1998","unstructured":"Mota A, Sampaio A. Model-checking CSP-Z. In: Proceedings of the 1st International Conference on Fundamental Approaches to Software Engineering (FASE). 1998, 205\u2013220"},{"key":"6192_CR131","first-page":"1","volume-title":"Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE).","author":"C Baier","year":"2014","unstructured":"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\u201316"},{"key":"6192_CR132","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/940071.940106","volume-title":"Proceedings of the 11th ESEC\/FSE.","author":"D Giannakopoulou","year":"2003","unstructured":"Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Proceedings of the 11th ESEC\/FSE. 2003, 257\u2013266"},{"key":"6192_CR133","first-page":"244","volume-title":"Proceedings of the 5th ESEC\/FSE.","author":"M B Dwyer","year":"1997","unstructured":"Dwyer M B, Carr V, Hines L. Model checking graphical user interfaces using abstractions. In: Proceedings of the 5th ESEC\/FSE. 1997, 244\u2013261"},{"key":"6192_CR134","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/940071.940097","volume-title":"Proceedings of the 11th ESEC\/FSE.","author":"O Tkachuk","year":"2003","unstructured":"Tkachuk O, Dwyer M B. Adapting side effects analysis for modular program model checking. In: Proceedings of the 11th ESEC\/FSE. 2003, 188\u2013197"},{"key":"6192_CR135","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1145\/503209.503232","volume-title":"Proceedings of the 9th ESEC\/FSE.","author":"Y Choi","year":"2001","unstructured":"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\u2013174"},{"key":"6192_CR136","first-page":"146","volume-title":"Proceedings of the 7th ESEC\/FSE.","author":"A Gargantini","year":"1999","unstructured":"Gargantini A, Heitmeyer C L. Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th ESEC\/FSE. 1999, 146\u2013162"},{"key":"6192_CR137","first-page":"400","volume-title":"Proceedings of the 21st ESEC\/FSE.","author":"F Zervoudakis","year":"2013","unstructured":"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\u2013410"},{"key":"6192_CR138","first-page":"607","volume-title":"Proceedings of the 21st ESEC\/FSE.","author":"F Song","year":"2013","unstructured":"Song F, Touili T. PoMMaDe: pushdown model-checking for mal ware detection. In: Proceedings of the 21st ESEC\/FSE. 2013, 607\u2013610"},{"key":"6192_CR139","first-page":"623","volume-title":"Proceedings of the 21st ESEC\/FSE.","author":"S Liu","year":"2013","unstructured":"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\u2013626"},{"key":"6192_CR140","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/940071.940107","volume-title":"Proceedings of the 11th ESEC\/FSE.","author":"Robby","year":"2003","unstructured":"Robby, Dwyer MB, Hatcliff J. Bogor: An extensible and highly modular software model checking framework. In: Proceedings of the 11th ESEC\/FSE. 2003, 267\u2013276"},{"issue":"5","key":"6192_CR141","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1387673.1387678","volume":"30","author":"M Naik","year":"2008","unstructured":"Naik M, Palsberg J. A type system equivalent to a model checker. ACM Transactions of Programming Languages and Systems, 2008, 30(5): 29","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"2","key":"6192_CR142","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1145\/244795.244803","volume":"19","author":"J Yang","year":"1997","unstructured":"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\u2013412","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"4","key":"6192_CR143","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"E A Emerson","year":"1997","unstructured":"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\u2013638","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"4","key":"6192_CR144","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1145\/1011508.1011511","volume":"26","author":"A P Sistla","year":"2004","unstructured":"Sistla A P, Godefroid P. Symmetry and reduced symmetry in model checking. ACM Transactions of Programming Languages and Systems, 2004, 26(4): 702\u2013734","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"4","key":"6192_CR145","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T Bultan","year":"1997","unstructured":"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\u2013789","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"5","key":"6192_CR146","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions of Programming Languages and Systems, 1994, 16(5): 1512\u20131542","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"3","key":"6192_CR147","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/2806886","volume":"38","author":"B Norris","year":"2016","unstructured":"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","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"2","key":"6192_CR148","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1348250.1348256","volume":"17","author":"S F Siegel","year":"2008","unstructured":"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","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"2","key":"6192_CR149","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1217295.1217296","volume":"16","author":"S Krishnamurthi","year":"2007","unstructured":"Krishnamurthi S, Fisler K. Foundations of incremental aspect modelchecking. ACM Transactions on Software Engineering and Methodology, 2007, 16(2): 7","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"3","key":"6192_CR150","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1243987.1243989","volume":"16","author":"R F Paige","year":"2007","unstructured":"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","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"3","key":"6192_CR151","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1243987.1243990","volume":"16","author":"S Basu","year":"2007","unstructured":"Basu S, Smolka S A. Model checking the Java metalocking algorithm. ACM Transactions on Software Engineering and Methodology, 2007, 16(3): 12","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"1","key":"6192_CR152","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1125808.1125809","volume":"15","author":"R Eshuis","year":"2006","unstructured":"Eshuis R. Symbolic model checking of UML activity diagrams. ACM Transactions on Software Engineering and Methodology, 2006, 15(1): 1\u201338","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"2","key":"6192_CR153","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/350887.350891","volume":"9","author":"A P Sistla","year":"2000","unstructured":"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\u2013166","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"4","key":"6192_CR154","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik M, Devereux B, Easterbrook SM, Gurfinkel A. Multi-valued symbolic model-checking. ACM Transactions on Software Engineering and Methodology, 2003, 12(4): 371\u2013408","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"6192_CR155","first-page":"157","volume-title":"Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"S F Siegel","year":"2006","unstructured":"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\u2013168"},{"key":"6192_CR156","first-page":"101","volume-title":"Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"L Gui","year":"2013","unstructured":"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\u2013111"},{"key":"6192_CR157","first-page":"252","volume-title":"Proceedings Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"X Fu","year":"2004","unstructured":"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\u2013262"},{"key":"6192_CR158","first-page":"423","volume-title":"Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"T Leesatapornwongsa","year":"2015","unstructured":"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\u2013427"},{"key":"6192_CR159","first-page":"102","volume-title":"Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"W Chan","year":"1998","unstructured":"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\u2013112"},{"key":"6192_CR160","first-page":"12","volume-title":"Proceedings of ACM International Symposium on Software Testing and Analysis (ISSTA).","author":"A Groce","year":"2002","unstructured":"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\u201321"},{"key":"6192_CR161","first-page":"61","volume-title":"Proceedings of the 41st POPL.","author":"S J Ramsay","year":"2014","unstructured":"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\u201372"},{"key":"6192_CR162","first-page":"110","volume-title":"Proceedings of the 32nd POPL.","author":"C Flanagan","year":"2005","unstructured":"Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd POPL. 2005, 110\u2013121"},{"key":"6192_CR163","first-page":"45","volume-title":"Proceedings of the 29th POPL.","author":"S Chaki","year":"2002","unstructured":"Chaki S, Rajamani S K, Rehof J. Types as models: model checking message-passing programs. In: Proceedings of the 29th POPL. 2002, 45\u201357"},{"key":"6192_CR164","first-page":"38","volume-title":"Proceedings of the 25th POPL","author":"D A Schmidt","year":"1998","unstructured":"Schmidt D A, Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th POPL. 1998, 38\u201348"},{"key":"6192_CR165","first-page":"174","volume-title":"Proceedings of the 24th POPL.","author":"P Godefroid","year":"1997","unstructured":"Godefroid P. Model checking for programming languages using Verisoft. In: Proceedings of the 24th POPL. 1997, 174\u2013186"},{"key":"6192_CR166","first-page":"342","volume-title":"Proceedings of the 19th POPL","author":"EM Clarke","year":"1992","unstructured":"Clarke EM, Grumberg O, Long D E. Model checking and abstraction. In: Proceedings of the 19th POPL. 1992, 342\u2013354"},{"issue":"5","key":"6192_CR167","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1109\/TC.2007.1021","volume":"56","author":"P-A Hsiung","year":"2007","unstructured":"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\u2013705","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"6192_CR168","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F He","year":"2010","unstructured":"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\u2013126","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"6192_CR169","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1109\/TC.2009.187","volume":"59","author":"H Zheng","year":"2010","unstructured":"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\u2013573","journal-title":"IEEE Transactions on Computers"},{"issue":"7","key":"6192_CR170","doi-asserted-by":"publisher","first-page":"1613","DOI":"10.1109\/TC.2013.63","volume":"63","author":"Y-R Chen","year":"2014","unstructured":"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\u20131625","journal-title":"IEEE Transactions on Computers"},{"issue":"6","key":"6192_CR171","first-page":"1607","volume":"64","author":"H Zheng","year":"2015","unstructured":"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\u20131621","journal-title":"IEEE Transactions on Computers"},{"key":"6192_CR172","first-page":"4","volume-title":"Proceedings of OOPSLA.","author":"M Roberson","year":"2010","unstructured":"Roberson M, Boyapati C. Efficient modular glass box software model checking. In: Proceedings of OOPSLA. 2010, 4\u201321"},{"key":"6192_CR173","first-page":"20","volume-title":"Proceedings of OOPSLA.","author":"B Demsky","year":"2015","unstructured":"Demsky B, Lam P. SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of OOPSLA. 2015, 20\u201336"},{"key":"6192_CR174","first-page":"57","volume-title":"Proceedings of OOPSLA.","author":"C S Jensen","year":"2015","unstructured":"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\u201373"},{"key":"6192_CR175","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1145\/1167473.1167504","volume-title":"Proceedings of OOPSLA.","author":"P T Darga","year":"2006","unstructured":"Darga P T, Boyapati C. Efficient software model checking of data structure properties. In: Proceedings of OOPSLA. 2006, 363\u2013382"},{"key":"6192_CR176","first-page":"493","volume-title":"Proceedings of OOPSLA.","author":"M Roberson","year":"2008","unstructured":"Roberson M, Harries M, Darga P T, Boyapati C. Efficient software model checking of soundness of type systems. In: Proceedings of OOPSLA. 2008, 493\u2013504"},{"key":"6192_CR177","first-page":"12","volume-title":"Proceedings of PLDI.","author":"S Burckhardt","year":"2007","unstructured":"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\u201321"},{"key":"6192_CR178","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1145\/2737924.2737975","volume-title":"Proceedings of PLDI.","author":"J Huang","year":"2015","unstructured":"Huang J. Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of PLDI. 2015, 165\u2013174"},{"key":"6192_CR179","first-page":"222","volume-title":"Proceedings of PLDI.","author":"N Kobayashi","year":"2011","unstructured":"Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI. 2011, 222\u2013233"},{"key":"6192_CR180","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/1375581.1375625","volume-title":"Proceedings of PLDI.","author":"M Musuvathi","year":"2008","unstructured":"Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of PLDI. 2008, 362\u2013371"},{"key":"6192_CR181","first-page":"200","volume-title":"Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering (ISSRE).","author":"Y Choi","year":"2011","unstructured":"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\u2013209"},{"key":"6192_CR182","first-page":"190","volume-title":"Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering (ISSRE).","author":"Y Liu","year":"2011","unstructured":"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\u2013199"},{"key":"6192_CR183","first-page":"51","volume-title":"Proceedings of the 23rd IEEE International Symposium on Software Reliability Engineering (ISSRE).","author":"Y J Kim","year":"2012","unstructured":"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\u201360"},{"key":"6192_CR184","first-page":"1","volume-title":"Proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM).","author":"D Letarte","year":"2010","unstructured":"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\u20132"},{"key":"6192_CR185","first-page":"115","volume-title":"Proceedings of the 25th IEEE International Conference on Software Maintenance (ICSM).","author":"G Yang","year":"2009","unstructured":"Yang G, Dwyer M B, Rothermel G. Regression model checking. In: Proceedings of the 25th IEEE International Conference on Software Maintenance (ICSM). 2009, 115\u2013124"},{"key":"6192_CR186","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/RE.2007.18","volume-title":"Proceedings of the 15th IEEE International Requirements Engineering Conference (RE)","author":"M Sabetzadeh","year":"2007","unstructured":"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\u2013230"},{"key":"6192_CR187","first-page":"174","volume-title":"Proceedings of the 9th IEEE International Requirements Engineering Conference (RE).","author":"A Fuxman","year":"2001","unstructured":"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\u2013181"},{"key":"6192_CR188","first-page":"193","volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"A Biere","year":"1999","unstructured":"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\u2013207"},{"key":"6192_CR189","volume-title":"Boston: Kluwer Academic Publishers","author":"K L McMillan","year":"1993","unstructured":"McMillan K L. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1993"},{"key":"6192_CR190","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1145\/302405.302710","volume-title":"Proceedings of the 21st International Conference on Software Engineering (ICSE).","author":"G J Holzmann","year":"1999","unstructured":"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\u2013607"},{"issue":"2","key":"6192_CR191","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G J Holzmann","year":"2000","unstructured":"Holzmann G J, Smith M H. Automating software feature verification. Bell Labs Technical Journal, 2000, 5(2): 72\u201387","journal-title":"Bell Labs Technical Journal"},{"key":"6192_CR192","first-page":"131","volume-title":"Proceedings of the 7th SPIN Workshop.","author":"G J Holzmann","year":"2000","unstructured":"Holzmann G J. Logic verification of ANSI-C code with SPIN. In: Proceedings of the 7th SPIN Workshop. 2000, 131\u2013147"},{"key":"6192_CR193","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/CSD.2001.981759","volume-title":"Proceedings of the 2nd International Conference on Application of Concurrency to System Design.","author":"G J Holzmann","year":"2001","unstructured":"Holzmann G J. From code to models. In: Proceedings of the 2nd International Conference on Application of Concurrency to System Design. 2001, 3\u201310"},{"issue":"4","key":"6192_CR194","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"G J Holzmann","year":"2002","unstructured":"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\u2013377","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6192_CR195","first-page":"76","volume-title":"Proceedings of the 11th SPIN Workshop.","author":"G J Holzmann","year":"2004","unstructured":"Holzmann G J, Joshi R. Model driven software verification. In: Proceedings of the 11th SPIN Workshop. 2004, 76\u201391"},{"issue":"2","key":"6192_CR196","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1142\/S0218213006002631","volume":"15","author":"M Wooldridge","year":"2006","unstructured":"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\u2013226","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"6192_CR197","first-page":"258","volume-title":"Proceedings of the 15th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS).","author":"T Vortler","year":"2012","unstructured":"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\u2013261"},{"key":"6192_CR198","first-page":"533","volume-title":"Proceedings of International Symposium on Formal Methods (FM).","author":"S Eisler","year":"2005","unstructured":"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\u2013536"},{"key":"6192_CR199","first-page":"7","volume-title":"Proceedings of the 10th MBT.","author":"A R Espada","year":"2015","unstructured":"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\u201321"},{"key":"6192_CR200","first-page":"199","volume-title":"Proceedings of the 3rd Mobile Cloud.","author":"L Aceto","year":"2015","unstructured":"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\u2013204"},{"key":"6192_CR201","first-page":"199","volume-title":"Proceedings of IEEE International Conference on Dependable Systems and Networks.","author":"Y W Huang","year":"2004","unstructured":"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\u2013208"},{"key":"6192_CR202","first-page":"361","volume-title":"Proceedings of the 3rd IEEE International Conference on Software Testing, Verification, and Validation Workshops.","author":"A Armando","year":"2010","unstructured":"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\u2013370"},{"key":"6192_CR203","first-page":"237","volume-title":"Proceedings on 11th ACIS International Conference on Software Engineering Artificial Intelligence Networking and Parallel\/Distributed Computing.","author":"L Li","year":"2010","unstructured":"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\u2013242"},{"key":"6192_CR204","first-page":"67","volume-title":"Proceedings of the 12th Asia-Pacific Software Engineering Conference.","author":"E H Choi","year":"2005","unstructured":"Choi E H, Watanabe H. Model checking class specifications for Web applications. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference. 2005, 67\u201378"},{"key":"6192_CR205","first-page":"69","volume-title":"Proceedings of the 5th International Conference on Web Engineering.","author":"E D Sciascio","year":"2005","unstructured":"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\u201374"},{"issue":"2","key":"6192_CR206","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2005.07.038","volume":"151","author":"S Nakajima","year":"2006","unstructured":"Nakajima S. Model-checking behavioral specification of BPEL applications. Electronic Notes in Theoretical Computer Science, 2006, 151(2): 19\u2013105","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6192_CR207","first-page":"1376","volume-title":"Proceedings of IFIP\/IEEE International Symposium on Integrated Network Management.","author":"C Ghezzi","year":"2013","unstructured":"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\u20131382"},{"key":"6192_CR208","first-page":"549","volume-title":"Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"M Gligoric","year":"2013","unstructured":"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\u2013564"},{"key":"6192_CR209","first-page":"296","volume-title":"Proceedings of the 8th SPIN Workshop.","author":"D D Cofer","year":"2001","unstructured":"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\u2013303"},{"key":"6192_CR210","first-page":"153","volume-title":"Proceedings of the 4th MOVEP.","author":"A Cimatti","year":"2000","unstructured":"Cimatti A. Industrial applications of model checking. In: Proceedings of the 4th MOVEP. 2000, 153\u2013168"},{"key":"6192_CR211","first-page":"54","volume-title":"Proceedings of the 2nd FTSCS Workshop.","author":"K A Hoque","year":"2013","unstructured":"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\u201370"},{"key":"6192_CR212","first-page":"1635","volume-title":"Proceedings the Design, Automation & Test in Europe Conference & Exhibition.","author":"K A Hoque","year":"2015","unstructured":"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\u20131640"},{"key":"6192_CR213","first-page":"31","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"A Armando","year":"2014","unstructured":"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\u201345"},{"key":"6192_CR214","volume-title":"Dissertation for the Doctoral Degree","author":"H Loding","year":"2014","unstructured":"Loding H. Model-based scenario testing and model checking with applications in the railway domain. Dissertation for the Doctoral Degree, 2014"},{"key":"6192_CR215","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.tcs.2015.11.040","volume":"623","author":"S Azimi","year":"2016","unstructured":"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\u2013113","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"6192_CR216","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/s10009-014-0343-0","volume":"17","author":"P Zuliani","year":"2015","unstructured":"Zuliani P. Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 527\u2013536","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6192_CR217","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-88562-7_18","volume-title":"Proceedings of International Conference on Computational Methods in Systems Biology.","author":"E M Clarke","year":"2008","unstructured":"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\u2013250"},{"key":"6192_CR218","first-page":"97","volume-title":"Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium.","author":"B Blackham","year":"2013","unstructured":"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\u2013106"},{"key":"6192_CR219","volume-title":"Proceedings on 12th USENEX Security Symposium","author":"M Christodorescu","year":"2003","unstructured":"Christodorescu M, Jha S. Static analysis of executables to detect malicious patterns. In: Proceedings on 12th USENEX Security Symposium. 2003"},{"key":"6192_CR220","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45510-8_1","volume-title":"Modelling and Verification of Parallel Processes","author":"S Merz","year":"2001","unstructured":"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\u201338"},{"key":"6192_CR221","first-page":"206","volume-title":"Proceeding of International Conference on Computer Science and Software Engineering.","author":"J Chen","year":"2008","unstructured":"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\u2013209"},{"key":"6192_CR222","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Proceedings of International Symposium on Theoretical Aspects of Computer Software.","author":"B Steffen","year":"1991","unstructured":"Steffen B. Data flow analysis as model checking. In: Proceedings of International Symposium on Theoretical Aspects of Computer Software. 1991, 346\u2013365"},{"issue":"8","key":"6192_CR223","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"R E Bryant","year":"1986","unstructured":"Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8), 677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"6192_CR224","first-page":"156","volume-title":"Proceedings of the 2nd International Conference on Computer Aided Verification (CAV).","author":"A Valmari","year":"1990","unstructured":"Valmari A. A stubborn attack on state explosion. In: Proceedings of the 2nd International Conference on Computer Aided Verification (CAV). 1990, 156\u2013165"},{"key":"6192_CR225","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Proceedings of the 5th International Conference on Computer Aided Verification (CAV).","author":"D A Peled","year":"1993","unstructured":"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\u2013423"},{"key":"6192_CR226","volume-title":"Dissertation for the Doctoral Degree","author":"P Godefroid","year":"1996","unstructured":"Godefroid P. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Dissertation for the Doctoral Degree, 1996"},{"key":"6192_CR227","first-page":"58","volume-title":"Proceedings of the 14th SPIN Workshop.","author":"Y Yang","year":"2007","unstructured":"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\u201375"},{"key":"6192_CR228","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-02658-4_31","volume-title":"Proceedings of the 21st International Conference on Computer Aided Verification (CAV).","author":"V Kahlon","year":"2009","unstructured":"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\u2013413"},{"key":"6192_CR229","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Proceedings of Formal Techniques for Distributed Systems.","author":"S Tasharofi","year":"2012","unstructured":"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\u2013234"},{"key":"6192_CR230","first-page":"373","volume-title":"Proceedings of the 41st POPL.","author":"P A Abdulla","year":"2014","unstructured":"Abdulla P A, Aronis S, Jonsson B, Sagonas K F. Optimal dynamic partial order reduction. In: Proceedings of the 41st POPL. 2014, 373\u2013384"},{"key":"6192_CR231","first-page":"108","volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design.","author":"M Sheeran","year":"2000","unstructured":"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\u2013125"},{"key":"6192_CR232","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV).","author":"K L McMillan","year":"2002","unstructured":"McMillan K L. Applying SATmethods in unbounded symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV). 2002, 250\u2013264"},{"key":"6192_CR233","first-page":"1","volume-title":"Proceedings of the 15th International Conference on Computer Aided Verification (CAV).","author":"K L McMillan","year":"2003","unstructured":"McMillan K L. Interpolation and SAT-based model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV). 2003, 1\u201313"},{"key":"6192_CR234","first-page":"510","volume-title":"Proceedings of IEEE\/ACM International Conference on Computer-aided Design.","author":"M K Ganai","year":"2004","unstructured":"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\u2013517"},{"key":"6192_CR235","first-page":"40","volume-title":"Proceedings of SPIN Workshop","author":"H Gunther","year":"2014","unstructured":"Gunther H, Weissenbacher G. Incremental bounded software model checking. In: Proceedings of SPIN Workshop, 2014, 40\u201347"},{"key":"6192_CR236","volume-title":"Proceedings of the 4th NASA Formal Methods.","author":"C Tinelli","year":"2012","unstructured":"Tinelli C. SMT-based model checking. In: Proceedings of the 4th NASA Formal Methods. 2012"},{"key":"6192_CR237","first-page":"97","volume-title":"Proceedings of the 23rd SPIN Workshop.","author":"M Garcia","year":"2016","unstructured":"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\u2013103"},{"key":"6192_CR238","first-page":"441","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"A Hinton","year":"2006","unstructured":"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\u2013444"},{"issue":"4","key":"6192_CR239","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-014-0349-7","volume":"17","author":"A Hartmanns","year":"2015","unstructured":"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\u2013456","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6192_CR240","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.08.009","volume":"649","author":"C Jegourel","year":"2016","unstructured":"Jegourel C, Legay A, Sedwards S. Command-based importance sampling for statistical model checking. Theoretical Computer Science, 2016, 649: 1\u201324","journal-title":"Theoretical Computer Science"},{"key":"6192_CR241","first-page":"23","volume-title":"Proceedings of the 11th SPIN Workshop.","author":"J Geldenhuys","year":"2004","unstructured":"Geldenhuys J. State caching reconsidered. In: Proceedings of the 11th SPIN Workshop. 2004, 23\u201338"},{"key":"6192_CR242","first-page":"7","volume-title":"Proceedings of TIME-ICTL.","author":"E M Clarke","year":"2003","unstructured":"Clarke E M. Counterexample-guided abstraction refinement. In: Proceedings of TIME-ICTL. 2003, 7\u20138"},{"key":"6192_CR243","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2013.04.007","volume":"295","author":"F Rabbi","year":"2013","unstructured":"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\u201393","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6192_CR244","first-page":"113","volume-title":"Proceedings of the 14th SPIN Workshop.","author":"J P Self","year":"2007","unstructured":"Self J P, Mercer E G. On-the-Fly dynamic dead variable analysis. In: Proceedings of the 14th SPIN Workshop. 2007, 113\u2013130"},{"key":"6192_CR245","first-page":"77","volume-title":"Proceedings of the 15th SPIN Workshop.","author":"S Evangelista","year":"2008","unstructured":"Evangelista S. Dynamic delayed duplicate detection for external memory model checking. In: Proceedings of the 15th SPIN Workshop. 2008, 77\u201394"},{"key":"6192_CR246","first-page":"162","volume-title":"Proceedings of the 17th SPIN Workshop.","author":"Z Chen","year":"2010","unstructured":"Chen Z, Motet G. Never trace claims for model checking. In: Proceedings of the 17th SPIN Workshop. 2010, 162\u2013179"},{"key":"6192_CR247","first-page":"221","volume-title":"Proceedings of the 9th SPIN Workshop.","author":"D Lugiez","year":"2002","unstructured":"Lugiez D, Niebert P, Zennou S. Dynamic bounds and transition merging for local first search. In: Proceedings of the 9th SPIN Workshop. 2002, 221\u2013229"},{"key":"6192_CR248","first-page":"1","volume-title":"Proceedings of the 3rd SPIN Workshop.","author":"G J Holzmann","year":"1997","unstructured":"Holzmann G J. State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of the 3rd SPIN Workshop. 1997, 1\u201310"},{"key":"6192_CR249","first-page":"232","volume-title":"Proceedings of the 15th SPIN Workshop.","author":"V Y Nguyen","year":"2008","unstructured":"Nguyen V Y, Ruys T C. Incremental hashing for Spin. In: Proceedings of the 15th SPIN Workshop. 2008, 232\u2013249"},{"key":"6192_CR250","first-page":"267","volume-title":"Proceedings of the 11th SPIN Workshop.","author":"M Rangarajan","year":"2004","unstructured":"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\u2013285"},{"key":"6192_CR251","first-page":"108","volume-title":"Proceedings of the 13th SPIN Workshop.","author":"I Melatti","year":"2006","unstructured":"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\u2013125"},{"key":"6192_CR252","first-page":"20","volume-title":"Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"K Laster","year":"1998","unstructured":"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\u201335"},{"issue":"4","key":"6192_CR253","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1016\/S1571-0661(05)80758-3","volume":"68","author":"L Brim","year":"2002","unstructured":"Brim L, Crhova J, Yorav K. Using assumptions to distribute CTL model checking. Electronic Notes in Theoretical Computer Science, 2002, 68(4): 559\u2013574","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6192_CR254","first-page":"1","volume-title":"Proceedings of IEEE International Parallel and Distributed Processing Symposium.","author":"G J Holzmann","year":"2007","unstructured":"Holzmann G J, Bosnacki D. Multi-core model checking with SPIN. In: Proceedings of IEEE International Parallel and Distributed Processing Symposium. 2007, 1\u20138"},{"key":"6192_CR255","first-page":"38","volume-title":"Proceedings of the 18th SPIN Workshop.","author":"A Laarman","year":"2011","unstructured":"Laarman A, Pol J, Weber M. Parallel recursive state compression for free. In: Proceedings of the 18th SPIN Workshop. 2011, 38\u201356"},{"key":"6192_CR256","first-page":"80","volume-title":"Proceedings of the 19th SPIN Workshop.","author":"A Ditter","year":"2012","unstructured":"Ditter A, Ceska M, Luttgen G. On parallel software verification using boolean equation systems. In: Proceedings of the 19th SPIN Workshop. 2012, 80\u201397"},{"key":"6192_CR257","first-page":"155","volume-title":"Proceedings of the 19th SPIN Workshop.","author":"G J Holzmann","year":"2012","unstructured":"Holzmann G J. Parallelizing the SPIN model checker. In: Proceedings of the 19th SPIN Workshop. 2012, 155\u2013171"},{"key":"6192_CR258","first-page":"172","volume-title":"Proceedings of the 19th SPIN Workshop.","author":"E Burns","year":"2012","unstructured":"Burns E, Zhou R. Parallel model checking using abstraction. In: Proceedings of the 19th SPIN Workshop. 2012, 172\u2013190"},{"key":"6192_CR259","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-73368-3_32","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV).","author":"J Barnat","year":"2007","unstructured":"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\u2013293"},{"key":"6192_CR260","first-page":"48","volume-title":"Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"J Barnat","year":"2008","unstructured":"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\u201362"},{"key":"6192_CR261","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","volume-title":"Proceedings of the 20th International Conference on Computer Aided Verification (CAV).","author":"S Edelkamp","year":"2008","unstructured":"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\u2013542"},{"issue":"5","key":"6192_CR262","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1109\/TVLSI.2014.2330061","volume":"23","author":"L Wu","year":"2015","unstructured":"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\u2013915","journal-title":"IEEE Transactions on Very Large Scale Integration Systems"},{"key":"6192_CR263","first-page":"786","volume-title":"Proceedings of IEEE\/ACM International Conference on Computer-Aided Design (ICCAD).","author":"M K Ganai","year":"2010","unstructured":"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\u2013793"},{"key":"6192_CR264","first-page":"43","volume-title":"Proceedings of the 19th SPIN Workshop.","author":"S Evangelista","year":"2012","unstructured":"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\u201361"},{"key":"6192_CR265","volume-title":"Proceedings of the 6th SPIN Workshop.","author":"K Havelund","year":"1999","unstructured":"Havelund K. Java Path Finder, a translator from Java to Promela. In: Proceedings of the 6th SPIN Workshop. 1999"},{"issue":"4","key":"6192_CR266","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"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\u2013425","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6192_CR267","first-page":"123","volume-title":"Proceedings of International Symposium on Formal Methods.","author":"J Sun","year":"2009","unstructured":"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\u2013139"},{"key":"6192_CR268","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-662-49674-9_20","volume-title":"Proceedings of the 22nd nternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"J Klein","year":"2016","unstructured":"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\u2013366"},{"issue":"3","key":"6192_CR269","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P Godefroid","year":"2012","unstructured":"Godefroid P, Levin M Y, Molnar D A. SAGE: white box fuzzing for security testing. Communications of the ACM, 2012, 55(3): 40\u201344","journal-title":"Communications of the ACM"},{"key":"6192_CR270","first-page":"235","volume-title":"Proceedings of the 10th SPIN Workshop.","author":"A H Thomas","year":"2003","unstructured":"Thomas A H, Ranjit J, Rupak M, Gregoire S. Software verification with BLAST. In: Proceedings of the 10th SPIN Workshop. 2003, 235\u2013239"},{"issue":"7","key":"6192_CR271","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"C K James","year":"1976","unstructured":"James C K. Symbolic execution and program testing. Communications of the ACM, 1976, 19(7): 385\u2013394","journal-title":"Communications of the ACM"},{"issue":"4","key":"6192_CR272","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1713254.1713257","volume":"43","author":"L Ciortea","year":"2010","unstructured":"Ciortea L, Zamfir C, Bucur S, Chipounov V, Candea G. Cloud9: a software testing service. ACM SIGOPS Operating Systems Review, 2010, 43(4): 5\u201310","journal-title":"ACM SIGOPS Operating Systems Review"},{"issue":"1","key":"6192_CR273","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/s11704-016-5459-9","volume":"12","author":"A K Karna","year":"2018","unstructured":"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\u2013100","journal-title":"Frontiers of Computer Science."},{"key":"6192_CR274","first-page":"553","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"S Khurshid","year":"2003","unstructured":"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\u2013568"},{"key":"6192_CR275","volume-title":"Dissertation for the Doctoral Degree","author":"H Amjad","year":"2004","unstructured":"Amjad H. Combining model checking and theorem proving. Dissertation for the Doctoral Degree, 2004"},{"key":"6192_CR276","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/10720084_11","volume-title":"Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS).","author":"T E Uribe","year":"2000","unstructured":"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\u2013170"},{"key":"6192_CR277","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-56922-7_13","volume-title":"Proceedings of the 5th International Conference on Computer Aided Verification (CAV).","author":"H Hungar","year":"1993","unstructured":"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\u2013165"},{"issue":"15","key":"6192_CR278","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.1016\/j.infsof.2004.07.002","volume":"46","author":"P Dybjer","year":"2004","unstructured":"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\u20131025","journal-title":"Information & Software Technology"},{"key":"6192_CR279","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2005.10.004","volume":"145","author":"H Amjad","year":"2006","unstructured":"Amjad H. Verification of AMBA using a combination of model checking and theorem proving. Electronic Notes in Theoretical Computer Science, 2006, 145: 45\u201361","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6192_CR280","first-page":"90","volume-title":"Proceedings of the 15th MTV Workshop.","author":"P Seidel","year":"2014","unstructured":"Seidel P. A case for multi-level combination of theorem proving and model checking tools. In: Proceedings of the 15th MTV Workshop. 2014, 90\u201397"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-016-6192-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6192-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6192-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T09:28:13Z","timestamp":1693646893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-016-6192-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,27]]},"references-count":280,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["6192"],"URL":"https:\/\/doi.org\/10.1007\/s11704-016-6192-0","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,27]]},"assertion":[{"value":"31 March 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 April 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}