{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:51Z","timestamp":1740099051454,"version":"3.37.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_18","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T10:02:34Z","timestamp":1520676154000},"page":"244-260","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Distributed Model Checking Using ProB"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)","edition":"1"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/BFb0020001","volume-title":"VDM 1991 Formal Software Development Methods","author":"J-R Abrial","year":"1991","unstructured":"Abrial, J.-R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., S\u00f8rensen, I.H.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398\u2013405. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0020001"},{"key":"18_CR3","unstructured":"Bagwell, P.: Ideal Hash Trees. Es Grands Champs, vol. 1195 (2001)"},{"key":"18_CR4","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":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-10373-5_26","volume-title":"Formal Methods and Software Engineering","author":"J Bendisposto","year":"2009","unstructured":"Bendisposto, J., Leuschel, M.: Proof assisted model checking for B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 504\u2013520. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_26"},{"key":"18_CR6","unstructured":"Bendisposto, J.M.: Directed and distributed model checking of B-specifications. Ph.D. thesis, Universit\u00e4ts- und Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2015)"},{"key":"18_CR7","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"},{"key":"18_CR8","volume-title":"SICStus Prolog User\u2019s Manual","author":"M Carlsson","year":"1988","unstructured":"Carlsson, M., Widen, J., Andersson, J., Andersson, S., Boortz, K., Nilsson, H., Sj\u00f6land, T.: SICStus Prolog User\u2019s Manual, vol. 3. Swedish Institute of Computer Science Kista, Sweden (1988)"},{"key":"18_CR9","unstructured":"DEPLOY Deliverable: D20-Report on Pilot Deployment in the Space Sector. FP7 ICT DEPLOY Project, January 2010. http:\/\/www.deploy-project.eu\/html\/deliverables.html"},{"key":"18_CR10","unstructured":"Ghemawat, S., Dean, J.: LevelDB (2011). https:\/\/github.com\/google\/leveldb"},{"key":"18_CR11","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-07512-9_5","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_5"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA $$^{+}$$ + to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-662-43652-3_4","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA $$^{+}$$ + for validation with TLC. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40\u201355. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_4"},{"key":"18_CR14","volume-title":"ZeroMQ: Messaging for Many Applications","author":"P Hintjens","year":"2013","unstructured":"Hintjens, P.: ZeroMQ: Messaging for Many Applications. O\u2019Reilly Media Inc., Newton (2013)"},{"issue":"5","key":"18_CR15","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR16","volume-title":"The Art of Computer Programming: Sorting and Searching","author":"DE Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming: Sorting and Searching, vol. III. Addison-Wesley, Boston (1973)"},{"key":"18_CR17","unstructured":"K\u00f6rner, P.: Improving distributed model checking in ProB. Bachelor\u2019s thesis, Heinrich Heine Universit\u00e4t D\u00fcsseldorf, August 2014"},{"key":"18_CR18","unstructured":"K\u00f6rner, P.: An integration of ProB and LTSmin. Master\u2019s thesis, Heinrich Heine Universit\u00e4t D\u00fcsseldorf, February 2017"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22\u201339. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48234-2_3"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-87603-8_2","volume-title":"Abstract State Machines, B and Z","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M.: The high road to formal validation: model checking high-level versus low-level specifications. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 4\u201323. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_2"},{"key":"18_CR21","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":"18_CR22","doi-asserted-by":"crossref","unstructured":"Prokopec, A., Bagwell, P., Odersky, M.: Cache-aware lock-free concurrent hash tries. arXiv preprint arXiv:1709.06056 (2017)","DOI":"10.1145\/3178487.3178498"},{"issue":"3","key":"18_CR23","doi-asserted-by":"crossref","first-page":"220","DOI":"10.2307\/2690615","volume":"67","author":"M Sayrafiezadeh","year":"1994","unstructured":"Sayrafiezadeh, M.: The birthday problem revisited. Math. Mag. 67(3), 220\u2013223 (1994)","journal-title":"Math. Mag."},{"issue":"4","key":"18_CR24","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/217391.217404","volume":"25","author":"C Venkatramani","year":"1995","unstructured":"Venkatramani, C., Chiueh, T.-C.: Design, implementation, and evaluation of a software-based real-time ethernet protocol. ACM SIGCOMM Comput. Commun. Rev. 25(4), 27\u201337 (1995)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"issue":"15","key":"18_CR25","doi-asserted-by":"crossref","first-page":"1547","DOI":"10.1016\/j.comcom.2004.04.003","volume":"27","author":"CK Yeo","year":"2004","unstructured":"Yeo, C.K., Lee, B.-S., Er, M.: A survey of application level multicast techniques. Comput. Commun. 27(15), 1547\u20131568 (2004)","journal-title":"Comput. Commun."},{"key":"18_CR26","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"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T13:01:53Z","timestamp":1570885313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}