{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T05:09:42Z","timestamp":1740114582505,"version":"3.37.3"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,4,25]],"date-time":"2010-04-25T00:00:00Z","timestamp":1272153600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s10009-010-0155-9","type":"journal-article","created":{"date-parts":[[2010,4,24]],"date-time":"2010-04-24T02:16:26Z","timestamp":1272075386000},"page":"89-95","source":"Crossref","is-referenced-by-count":3,"title":["Model checking software: on some new waves and some evergreens"],"prefix":"10.1007","volume":"12","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,4,25]]},"reference":[{"key":"155_CR1","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier C., Katoen J-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"155_CR2","doi-asserted-by":"crossref","unstructured":"Verstoep, K., Bal, H., Barnat, J., Brim. L.: Efficient large-scale model checking. In: Proceedings of the 23rd IEEE International Symposium on Parallel and Distributed Processing (IPDPS), pp. 1\u201312. IEEE Computer Society, USA (2009)","DOI":"10.1109\/IPDPS.2009.5161000"},{"key":"155_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Proceedings of the 13th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2102, pp. 260\u2013264. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"key":"155_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable shared memory LTL model checking. STTT, this volume. Springer, Berlin (2010)","DOI":"10.1007\/s10009-010-0136-z"},{"key":"155_CR5","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek P.: I\/O efficient accepting cycle detection. In: Proceedings of the 13th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 281\u2013293. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_32"},{"key":"155_CR6","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P., Weber, M.: Revisiting resistance speeds up 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). Lecture Notes in Computer Science, vol. 4963, pp. 48\u201362 (2008)","DOI":"10.1007\/978-3-540-78800-3_5"},{"key":"155_CR7","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Str\u00edbrn\u00e1, J.: Distributed LTL model checking in SPIN. In: Proceedings of the 8th International Spin Workshop on Model Checking of Software (SPIN). Lecture Notes in Computer Science, vol. 2057, pp. 200\u2013216. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_13"},{"key":"155_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT, vol. 9 (5\u20136), pp. 505\u2013525. Springer, Berlin (2007)","DOI":"10.1007\/s10009-007-0044-z"},{"key":"155_CR9","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S.: In: Proceedings of the 14th International Spin Workshop on Model Checking of Software (SPIN). Lecture Notes in Computer Science, vol. 4595. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73370-6"},{"key":"155_CR10","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: Proceedings of the 16th International Spin Workshop on Model Checking of Software (SPIN). Lecture Notes in Computer Science, vol. 5578, pp. 32-49. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02652-2_7"},{"issue":"5","key":"155_CR11","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke E.M., Grumberg O., Jha S., Lu Y., Veith H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"155_CR12","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumber O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"155_CR13","doi-asserted-by":"crossref","unstructured":"Cleaveland, R.: Pragmatics of model checking: an STTT special section. STTT, vol. 2(3). Springer, Berlin (1999)","DOI":"10.1007\/s100090050030"},{"key":"155_CR14","doi-asserted-by":"crossref","unstructured":"Corbet, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Zheng, Robby H.: Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd IEEE International Conference on Software Engineering (ICSE), pp. 439\u2013448. IEEE Computer Society, USA (2000)","DOI":"10.1145\/337180.337234"},{"key":"155_CR15","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Leue, S.: Introductory paper. STTT, vol. 6(4), pp. 257\u2013259. Springer, Berlin (2004)","DOI":"10.1007\/s10009-004-0168-3"},{"key":"155_CR16","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Proceedings of the 13th International Spin Workshop on Model Checking of Software, (SPIN). Lecture Notes in Computer Science, vol. 3925, pp. 1\u201318. Springer, Berlin (2006)","DOI":"10.1007\/11691617_1"},{"key":"155_CR17","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sanders, P., \u0160ime\u010dek P.: Semi-external LTL model checking. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 5123, pp. 530\u2013542. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_50"},{"key":"155_CR18","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 73\u201382. IEEE International, USA (2008)","DOI":"10.1109\/SEFM.2008.34"},{"key":"155_CR19","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson E.A.: Temporal and modal logic. In: van Leeuwen, J. (eds) Handbook of Theoretical Computer Science, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"155_CR20","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proceedings of the 7th Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 85, pp. 169\u2013181. Springer, Berlin (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"155_CR21","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. STTT, this volume. Springer, Berlin (2010)","DOI":"10.1007\/s10009-010-0137-y"},{"key":"155_CR22","unstructured":"Fecher, H., Shoham, S.: Local abstraction-refinement for the mu-calculus. STTT, this volume. Springer, Berlin (2010)"},{"key":"155_CR23","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of concurrent Systems\u2014An Approach to the State Space Explosion. Lecture Notes in Computer Science, vol. 1032. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60761-7"},{"issue":"2","key":"155_CR24","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"155_CR25","unstructured":"Hajek, J.: Automatically verified data transfer protocols. In: Proceedings of the 4th International Computer Communications Conference, pp. 749\u2013756 (1978)"},{"key":"155_CR26","doi-asserted-by":"crossref","unstructured":"Havelund, K., Visser, W.: Program model checking as a new trend. STTT, vol. 4(1), pp. 8\u201320. Springer, Berlin (2002)","DOI":"10.1007\/s10009-002-0080-7"},{"key":"155_CR27","volume-title":"Designing executable abstractions. In: Proceedings of Formal Methods in Software Practice","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann G.J.: Designing executable abstractions. In: Proceedings of Formal Methods in Software Practice. ACM Press, Clearwater Beach Florida USA (1998)"},{"key":"155_CR28","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Reading (2003)"},{"issue":"10","key":"155_CR29","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann G.J., Bo\u0161na\u010dki D.: The Design of a multi-core extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"155_CR30","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: Multi-core model checking with SPIN. In: Proceedings of the IEEE International Symposium on Parallel and Distributed Processing (IPDPS), pp. 1\u20138. IEEE Computer Society, USA (2007)","DOI":"10.1109\/IPDPS.2007.370410"},{"issue":"2","key":"155_CR31","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"G.J. Holzmann","year":"2001","unstructured":"Holzmann G.J., Smith M.H.: Software model checking\u2014extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 65\u201379 (2001)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"4","key":"155_CR32","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.entcs.2004.10.022","volume":"128","author":"C.P. Inggs","year":"2005","unstructured":"Inggs C.P., Barringer H.: CTL* model checking on a shared memory architecture. Electron. Notes Theor. Comput. Sci. 128(4), 107\u2013123 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"155_CR33","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1016\/S1571-0661(05)80395-0","volume":"68","author":"C.P. Inggs","year":"2002","unstructured":"Inggs C.P., Barringer H.: Effective state exploration for model checking on a shared memory architecture. Electron. Notes Theor. Comput. Sci. 68(4), 605\u2013620 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"155_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala R., Majumdar R.: Software model checking. ACM Comput. Surv. 41(4), 1\u201354 (2009)","journal-title":"ACM Comput. Surv."},{"key":"155_CR35","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen D.: Results on the propositional\u00a0\u03bc-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"155_CR36","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sisto, R.: Distributed model checking in SPIN. Theoretical and Practical Aspects of SPIN Model Checking. In: Proceedings of the 5th and 6th International SPIN Workshops. Lecture Notes in Computer Science, vol. 1680, pp. 22\u201339. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48234-2_3"},{"key":"155_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna Z., Pnueli A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)"},{"issue":"9","key":"155_CR38","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1284621.1284622","volume":"50","author":"A. Marowka","year":"2007","unstructured":"Marowka A.: Parallel computing on any desktop. Commun. ACM 50(9), 75\u201378 (2007)","journal-title":"Commun. ACM"},{"key":"155_CR39","unstructured":"Moore, G.E.: Cramming more components onto integrated circuits. Readings in Computer Architecture, pp. 56\u201359. Morgan Kaufmann, San Francisco (2000)"},{"key":"155_CR40","unstructured":"OpenMP Architecture Review Board. OpenMP Application Program Interface, Version 2.5 (May 2005). http:\/\/www.openm.org"},{"key":"155_CR41","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D.A. Peled","year":"1996","unstructured":"Peled D.A.: Combining partial-order reductions with on-the-fly model checking. Formal Methods Syst. Des. 8, 39\u201364 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"155_CR42","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, vol. 137, pp. 337\u2013350. Springer, Berlin (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"155_CR43","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. STTT, this volume. Springer, Berlin (2010)","DOI":"10.1007\/s10009-010-0140-3"},{"key":"155_CR44","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.: Parallelizing the Mur $${\\phi}$$ verifier. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1254, pp. 256\u2013278. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"155_CR45","doi-asserted-by":"crossref","unstructured":"Willems, B., Wolper, P.: Partial-order methods for model checking: from linear to branching time. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 294\u2013303. IEEE Computer Society, USA (1996)","DOI":"10.1109\/LICS.1996.561357"},{"key":"155_CR46","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Proceedings of the Second Parallel Architectures and Languages Europe (PARLE). Lecture Notes in Computer Science, vol. 366, pp. 89\u2013103. Springer, Berlin (1989)","DOI":"10.1007\/3-540-51285-3_35"},{"key":"155_CR47","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. Advances in Petri Nets. Lecture Notes in Computer Science, vol. 531, pp. 156\u2013165. Springer, Berlin (1991)","DOI":"10.1007\/BFb0023729"},{"key":"155_CR48","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. Lectures on Petri Nets I: Basic Models, LNCS Tutorials. Lecture Notes in Computer Science, vol. 1491, pp. 429\u2013528. Springer, Berlin (1998)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"155_CR49","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Software model checking is a rich research field. STTT, vol. 11(1), pp. 1\u201311. Springer, Berlin (2009)","DOI":"10.1007\/s10009-008-0089-7"},{"key":"155_CR50","doi-asserted-by":"crossref","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 (ICSE), pp. 3\u201312. IEEE Computer Society, USA (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"155_CR51","doi-asserted-by":"crossref","unstructured":"Weber, M.: An embeddable virtual machine for state space generation. STTT, this volume. Springer, Berlin (2010)","DOI":"10.1007\/s10009-010-0141-2"},{"key":"155_CR52","doi-asserted-by":"crossref","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby R.M.: Distributed dynamic partial order reduction. STTT, this volume. Springer, Berlin (2010)","DOI":"10.1007\/s10009-010-0144-z"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0155-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0155-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0155-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:07:00Z","timestamp":1740028020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0155-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,25]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["155"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0155-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2010,4,25]]}}}