{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T19:05:00Z","timestamp":1771614300432,"version":"3.50.1"},"publisher-location":"Cham","reference-count":77,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319919072","type":"print"},{"value":"9783319919089","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_20","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T09:05:00Z","timestamp":1570179900000},"page":"393-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Software Architecture of Modern Model Checkers"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Kordon","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"20_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"1","key":"20_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028774"},{"issue":"2\u20133","key":"20_CR5","doi-asserted-by":"crossref","first-page":"109","DOI":"10.3233\/FI-1999-402302","volume":"40","author":"A Arnold","year":"1999","unstructured":"Arnold, A., Point, G., Griffault, A., Rauzy, A.: The altarica formalism for describing concurrent systems. Fundam. Inform. 40(2\u20133), 109\u2013124 (1999)","journal-title":"Fundam. Inform."},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"20_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"20_CR8","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th IW on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"20_CR9","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125\u2013126. IEEE Computer Society (2006)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-33693-0_18","volume-title":"Integrated Formal Methods","author":"J Bendisposto","year":"2016","unstructured":"Bendisposto, J., K\u00f6rner, P., Leuschel, M., Meijer, J., van de Pol, J., Treharne, H., Whitefield, J.: Symbolic reachability analysis of B through ProB and LTSmin. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 275\u2013291. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_18"},{"key":"20_CR11","unstructured":"Berthomieux, B., Bodeveix, J.P., Filali, M., Lang, F., Le Botland, D., Vernadat, F.: The syntax and semantic of fiacre. Technical report 7264, CNRS-LAAS (2007)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"issue":"1","key":"20_CR13","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1093\/logcom\/exp004","volume":"21","author":"S Blom","year":"2011","unstructured":"Blom, S., Lisser, B., van de Pol, J., Weber, M.: A database approach to distributed state-space generation. J. Log. Comput. 21(1), 45\u201362 (2011)","journal-title":"J. Log. Comput."},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_31"},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"RH Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Auton. Agent. Multi-Agent Syst. 12(2), 239\u2013256 (2006)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2007.03.017","volume":"184","author":"RM Borges","year":"2007","unstructured":"Borges, R.M., Mota, A.C.: Integrating UML and formal methods. Electron. Notes Theor. Comput. Sci. 184, 97\u2013112 (2007). 2nd Brazilian Symposium on Formal Methods (SBMF 2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11526841_16","volume-title":"FM 2005: Formal Methods","author":"M Butler","year":"2005","unstructured":"Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221\u2013236. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11526841_16"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"36","DOI":"10.4204\/EPTCS.115.3","volume":"115","author":"Michael Butler","year":"2013","unstructured":"Butler, M.J., Colley, J., Edmunds, A., Snook, C.F., Evans, N., Grant, N., Marshall, H.: Modelling and refinement in CODA. In: Derrick, J., Boiten, E.A., Reeves, S. (eds.) Proceedings 16th International Refinement Workshop, Refine@IFM 2013, Turku, Finland, 11 June 2013. EPTCS, vol. 115, pp. 36\u201351 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"issue":"11","key":"20_CR20","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging (turing award 2007). Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Correa, T., Becker, L.B., Farines, J., Bodeveix, J., Filali, M., Vernadat, F.: Supporting the design of safety critical systems using AADL. In: 15th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, pp. 331\u2013336. IEEE Computer Society (2010)","DOI":"10.1109\/ICECCS.2010.56"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223\u2013239. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_16"},{"issue":"3","key":"20_CR24","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G Delzanno","year":"2001","unstructured":"Delzanno, G., Podelski, A.: Constraint-based deductive model checking. STTT 3(3), 250\u2013270 (2001)","journal-title":"STTT"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk van","year":"2015","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$ -automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"20_CR27","unstructured":"Eclipse Project: Model-to-Model Transformation MMT, subproject of Eclipse Modeling (2017). https:\/\/projects.eclipse.org\/projects\/modeling.mmt"},{"key":"20_CR28","unstructured":"Efftinge, S., et al.: XText (2017). http:\/\/www.eclipse.org\/Xtext\/"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite-state systems by specializing constraint logic programs. In: Proceedings of VCL 2001, Florence, Italy, September 2001","DOI":"10.1007\/3-540-45142-0_8"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68\u201384. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054165"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-19488-2_9","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"H Garavel","year":"2015","unstructured":"Garavel, H.: Nested-unit petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 179\u2013199. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19488-2_9"},{"issue":"4\u20135","key":"20_CR32","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s00236-015-0226-1","volume":"52","author":"H Garavel","year":"2015","unstructured":"Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Inf. 52(4\u20135), 337\u2013392 (2015)","journal-title":"Acta Inf."},{"key":"20_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05324-9","volume-title":"Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications","author":"C Girault","year":"2003","unstructured":"Girault, C., Valk, R.: Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-662-05324-9"},{"issue":"1\u20132","key":"20_CR34","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","volume":"48","author":"JF Groote","year":"2001","unstructured":"Groote, J.F., Ponse, A., Usenko, Y.S.: Linearization in parallel pcrl. J. Log. Algebr. Program. 48(1\u20132), 39\u201370 (2001)","journal-title":"J. Log. Algebr. Program."},{"issue":"4","key":"20_CR35","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000). https:\/\/doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"6","key":"20_CR36","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1049\/sej.1989.0045","volume":"4","author":"I Hayes","year":"1989","unstructured":"Hayes, I., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330\u2013338 (1989)","journal-title":"Softw. Eng. J."},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545\u2013558. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_103"},{"issue":"8","key":"20_CR38","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"20_CR39","volume-title":"Spin Model Checker, The: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"20_CR40","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)"},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-40793-2_12","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2013","unstructured":"Iliasov, A., Lopatkin, I., Romanovsky, A.: The SafeCap platform for modelling railway safety and capacity. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 130\u2013137. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_12"},{"key":"20_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-662-53401-4_12","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"F Kordon","year":"2016","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Paviot-Adet, E., Jezequel, L., Rodr\u00edguez, C., Hulin-Hubard, F.: MCC\u20192015 \u2013 the fifth model checking contest. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 262\u2013273. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_12"},{"key":"20_CR44","unstructured":"K\u00f6rner, P.: An integration of ProB and LTSmin. Master\u2019s thesis, Universit\u00e4t D\u00fcsseldorf, February 2017"},{"key":"20_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"20_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"968","DOI":"10.1007\/978-3-642-39799-8_69","volume-title":"Computer Aided Verification","author":"A Laarman","year":"2013","unstructured":"Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multi-core emptiness checking of timed B\u00fcchi automata using inclusion abstraction. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 968\u2013983. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_69"},{"issue":"4","key":"20_CR47","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s10009-014-0363-9","volume":"18","author":"A Laarman","year":"2016","unstructured":"Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. STTT 18(4), 427\u2013448 (2016)","journal-title":"STTT"},{"key":"20_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-642-20398-5_40","volume-title":"NASA Formal Methods","author":"A Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506\u2013511. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_40"},{"key":"20_CR49","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"20_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"20_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-88194-0_18","volume-title":"Formal Methods and Software Engineering","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Fontaine, M.: Probing the depths of CSP-M: a new fdr-compliant validation tool. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 278\u2013297. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_18"},{"key":"20_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/10720327_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M Leuschel","year":"2000","unstructured":"Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 62\u201381. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720327_5"},{"key":"20_CR53","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: IEEE 22nd International Symposium on Software Reliability Engineering, ISSRE 2011, Hiroshima, Japan, 29 November\u20132 December 2011, pp. 190\u2013199 (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"issue":"1\u20132","key":"20_CR54","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1\u20132), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137\u2013151. ACM (1987)","DOI":"10.1145\/41840.41852"},{"key":"20_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/978-3-540-31980-1_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Margaria","year":"2005","unstructured":"Margaria, T., Nagel, R., Steffen, B.: jETI: a tool for remote tool integration. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 557\u2013562. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_38"},{"key":"20_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-13338-6_16","volume-title":"Hardware and Software: Verification and Testing","author":"J Meijer","year":"2014","unstructured":"Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 204\u2013219. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_16"},{"issue":"4\u20135","key":"20_CR58","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s00165-008-0082-7","volume":"20","author":"R Meyer","year":"2008","unstructured":"Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model checking duration calculus: a practical approach. Formal Asp. Comput. 20(4\u20135), 481\u2013505 (2008)","journal-title":"Formal Asp. Comput."},{"key":"20_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-48234-2_14","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"CS P\u0103s\u0103reanu","year":"1999","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 168\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48234-2_14"},{"key":"20_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/10722167_48","volume-title":"Computer Aided Verification","author":"CR Ramakrishnan","year":"2000","unstructured":"Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Dong, Y., Du, X., Roychoudhury, A., Venkatakrishnan, V.N.: XMC: a logic-programming-based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 576\u2013580. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_48"},{"key":"20_CR61","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1999","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1999)"},{"key":"20_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AW Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133\u2013152. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_7"},{"key":"20_CR63","unstructured":"Samia, M., Wiegard, H., Bendisposto, J., Leuschel, M.: High-level versus low-level specifications: comparing B with Promela and ProB with spin. In: Proceedings TFM-B 2009, pp. 49\u201361. APCB, June 2009"},{"key":"20_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-44919-1_29","volume-title":"Applications and Theory of Petri Nets 2003","author":"C Schr\u00f6ter","year":"2003","unstructured":"Schr\u00f6ter, C., Schwoon, S., Esparza, J.: The model-checking kit. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 463\u2013472. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44919-1_29"},{"key":"20_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-87603-8_32","volume-title":"Abstract State Machines, B and Z","author":"C Snook","year":"2008","unstructured":"Snook, C., Butler, M.: UML-B: a plug-in for the Event-B tool set. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 344. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_32"},{"key":"20_CR66","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Upper Saddle River (1992)"},{"issue":"1","key":"20_CR67","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10270-012-0272-x","volume":"13","author":"A Stefanescu","year":"2014","unstructured":"Stefanescu, A., Wieczorek, S., Schur, M.: Message choreography modeling. Softw. Syst. Model. 13(1), 9\u201333 (2014)","journal-title":"Softw. Syst. Model."},{"key":"20_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995: Concurrency Theory","author":"B Steffen","year":"1995","unstructured":"Steffen, B., Cla\u00dfen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72\u201387. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_6"},{"issue":"1\u20132","key":"20_CR69","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s100090050003","volume":"1","author":"B Steffen","year":"1997","unstructured":"Steffen, B., Margaria, T., Braun, V.: The electronic tool integration platform: concepts and design. STTT 1(1\u20132), 9\u201330 (1997)","journal-title":"STTT"},{"key":"20_CR70","volume-title":"EMF: Eclipse Modeling Framework 2.0","author":"D Steinberg","year":"2009","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework 2.0, 2nd edn. Addison-Wesley Professional, Boston (2009)","edition":"2"},{"key":"20_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"},{"issue":"4","key":"20_CR72","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR73","unstructured":"Voelter, M., et al.: DSL Engineering - Designing, Implementing and Using Domain-Specific Languages (2013). dslbook.org"},{"key":"20_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11526841_17","volume-title":"FM 2005: Formal Methods","author":"J Woodcock","year":"2005","unstructured":"Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 237\u2013252. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11526841_17"},{"issue":"1","key":"20_CR75","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10009-015-0402-1","volume":"19","author":"K Ye","year":"2017","unstructured":"Ye, K., Woodcock, J.: Model checking of state-rich formalism Circus by linking to CSP $$\\Vert $$ B. STTT 19(1), 73\u201396 (2017)","journal-title":"STTT"},{"key":"20_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"},{"issue":"1","key":"20_CR77","first-page":"1","volume":"12","author":"H Zhu","year":"2016","unstructured":"Zhu, H., Sun, J., Dong, J.S., Lin, S.: From verified model to executable program: the PAT approach. ISSE 12(1), 1\u201326 (2016)","journal-title":"ISSE"}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,24]],"date-time":"2021-01-24T04:34:52Z","timestamp":1611462892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":77,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}