{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:37:40Z","timestamp":1743107860815,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_15","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"212-226","source":"Crossref","is-referenced-by-count":6,"title":["Multi-core Model Checking of Large-Scale Reactive Systems Using Different State Representations"],"prefix":"10.1007","author":[{"given":"Marc","family":"Jasper","sequence":"first","affiliation":[]},{"given":"Markus","family":"Schordan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1109\/TASE.2006.880857","volume":"4","author":"EE Almeida","year":"2007","unstructured":"Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-condition-action systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167\u2013181 (2007)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"5","key":"15_CR2","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. SIGPLAN Not. 36(5), 203\u2013213 (2001)","journal-title":"SIGPLAN Not."},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, p. 57. ACM (2012)","key":"15_CR5","DOI":"10.1145\/2393596.2393664"},{"issue":"5","key":"15_CR6","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10009-014-0334-1","volume":"16","author":"D Beyer","year":"2014","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event-condition-action systems. Intl. J. Softw. Tools Technol. Transf. 16(5), 507\u2013518 (2014)","journal-title":"Intl. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"15_CR7","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.-J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"15_CR8","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Workshop on Logic of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, A.E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Workshop on Logic of Programs. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"issue":"5","key":"15_CR10","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 265\u2013276. ACM, New York (2007)","key":"15_CR12","DOI":"10.1145\/1190216.1190257"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/978-3-662-46681-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 384\u2013398. Springer, Heidelberg (2015)"},{"doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: The IEEE Computer Society\u2019s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004 (MASCOTS 2004), pp. 76\u201383. IEEE (2004)","key":"15_CR14","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"15_CR16","volume-title":"The SPIN Model Checker Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)","edition":"1"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-642-31759-0_12","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2012","unstructured":"Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 155\u2013171. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bosnacki, D.: Multi-core model checking with SPIN. In: Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, pp. 1\u20138, March 2007","key":"15_CR18","DOI":"10.1109\/IPDPS.2007.370410"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1007\/978-3-642-34026-0_45","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"F Howar","year":"2012","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 608\u2013614. Springer, Heidelberg (2012)"},{"issue":"3","key":"15_CR20","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2004.10.016","volume":"128","author":"R Kumar","year":"2005","unstructured":"Kumar, R., Mercer, E.G.: Load balancing parallel explicit state model checking. Electron. Notes in Theor. Comput. Sci. 128(3), 19\u201334 (2005)","journal-title":"Electron. Notes in Theor. Comput. Sci."},{"issue":"2","key":"15_CR21","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/66926.66946","volume":"18","author":"D McCarthy","year":"1989","unstructured":"McCarthy, D., Dayal, U.: The architecture of an active database management system. ACM Sigmod Rec. 18(2), 215\u2013224 (1989). ACM","journal-title":"ACM Sigmod Rec."},{"issue":"5","key":"15_CR22","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-014-0335-0","volume":"16","author":"J Morse","year":"2014","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS greybox challenge. Intl. J. Softw. Tools Technol. Transf. 16(5), 519\u2013529 (2014)","journal-title":"Intl. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1998, pp. 38\u201348. ACM, New York (1998)","key":"15_CR23","DOI":"10.1145\/268946.268950"},{"issue":"5","key":"15_CR24","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/s10009-014-0338-x","volume":"16","author":"M Schordan","year":"2014","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Intl. J. Softw. Tools Technol. Transf. 16(5), 493\u2013505 (2014)","journal-title":"Intl. J. Softw. Tools Technol. Transf."},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-45213-3_27","volume-title":"Modular Programming Languages","author":"M Schordan","year":"2003","unstructured":"Schordan, M., Quinlan, D.: A source-to-source architecture for user-defined optimizations. In: B\u00f6sz\u00f6rm\u00e9nyi, L., Schojer, P. (eds.) JMLC 2003. LNCS, vol. 2789, pp. 214\u2013223. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45213-3_27"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346\u2013364. Springer, Heidelberg (1991). doi: 10.1007\/3-540-54415-1_54"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"International Static Analysis Symposium","author":"B Steffen","year":"1996","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) International Static Analysis Symposium. LNCS, vol. 1145, pp. 22\u201341. Springer, Heidelberg (1996)"},{"issue":"5","key":"15_CR28","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Softw. Tools Technol. Transf. 16(5), 465\u2013479 (2014)","journal-title":"Softw. Tools Technol. Transf."},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models. Advances in Petri Nets","author":"A Valmari","year":"1998","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429\u2013528. Springer, Heidelberg (1998)"},{"issue":"5","key":"15_CR30","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/s10009-014-0324-3","volume":"16","author":"J Pol van de","year":"2014","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful Brute-force attack of the RERS 2012 and 2013 challenges. Intl. J. Softw. Tools Technol. Transf. 16(5), 481\u2013491 (2014)","journal-title":"Intl. J. Softw. Tools Technol. Transf."},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11537328_5","volume-title":"Model Checking Software","author":"W Visser","year":"2005","unstructured":"Visser, W., Mehlitz, P.: Model checking programs with Java pathfinder. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 27\u201327. Springer, Heidelberg (2005). doi: 10.1007\/11537328_5"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:22:05Z","timestamp":1498335725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}