{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:37:37Z","timestamp":1725856657171},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"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-33693-0_18","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:35:47Z","timestamp":1464068147000},"page":"275-291","source":"Crossref","is-referenced-by-count":8,"title":["Symbolic Reachability Analysis of B Through ProB and LTSmin"],"prefix":"10.1007","author":[{"given":"Jens","family":"Bendisposto","sequence":"first","affiliation":[]},{"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"Jeroen","family":"Meijer","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[]},{"given":"Jorden","family":"Whitefield","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","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)"},{"key":"18_CR2","volume-title":"The B-Book - Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-642-11811-1_6","volume-title":"Abstract State Machines, Alloy, B and Z","author":"P Arcaini","year":"2010","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61\u201374. Springer, Heidelberg (2010)"},{"key":"18_CR4","unstructured":"Bendisposto, J.: Directed and Distributed Model Checking of B Specifications. Ph.D. thesis, University of D\u00fcsseldorf (2015). http:\/\/docserv.uni-duesseldorf.de\/servlets\/DocumentServlet?id=34472"},{"key":"18_CR5","doi-asserted-by":"crossref","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. CoRR abs\/1603.04401 (2016)","DOI":"10.1007\/978-3-319-33693-0_18"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"810","DOI":"10.1007\/978-3-642-05089-3_52","volume-title":"FM 2009: Formal Methods","author":"JC Bicarregui","year":"2009","unstructured":"Bicarregui, J.C., Fitzgerald, J.S., Larsen, P.G., Woodcock, J.C.P.: Industrial practice in formal methods: a review. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 810\u2013813. Springer, Heidelberg (2009)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-540-85762-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"S Blom","year":"2008","unstructured":"Blom, S., van de Pol, J.: Symbolic reachability for process algebras with recursive data types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81\u201395. Springer, Heidelberg (2008)"},{"issue":"2","key":"18_CR8","first-page":"142","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}$$ 10 20 states and beyond. IC 98(2), 142\u2013170 (1992)","journal-title":"IC"},{"issue":"1","key":"18_CR9","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. STTT 8(1), 4\u201325 (2006)","journal-title":"STTT"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-87603-8_22","volume-title":"Abstract State Machines, B and Z","author":"J Derrick","year":"2008","unstructured":"Derrick, J., North, S., Simons, A.J.H.: Z2SAL - building a model checker for Z. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 280\u2013293. Springer, Heidelberg (2008)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-319-10431-7_16","volume-title":"Software Engineering and Formal Methods","author":"I Dobrikov","year":"2014","unstructured":"Dobrikov, I., Leuschel, M.: Optimising the ProB model checker for B using partial order reduction. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 220\u2013234. Springer, Heidelberg (2014)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 $$^ \\text{+ } $$ + for validation with TLC. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40\u201355. Springer, Heidelberg (2014)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-38697-8_21","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Heiner","year":"2013","unstructured":"Heiner, M., Rohr, C., Schwarick, M.: MARCIE \u2013 model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389\u2013399. Springer, Heidelberg (2013)"},{"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, Sebastopol (2013)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"H\u00f6rne, T., van der Poll, J.A.: Planning as model checking: the performance of ProB vs NuSMV. In: SAICSIT Conference ACM ICPS, vol. 338, pp. 114\u2013123. ACM (2008)","DOI":"10.1145\/1456659.1456673"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-319-05032-4_15","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP $$||$$ | | B. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189\u2013204. Springer, Heidelberg (2014)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Laarman, A., Pater, E., Pol, J., Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transfer, 1\u201322 (2014). doi: 10.1007\/s10009-014-0363-9","DOI":"10.1007\/s10009-014-0363-9"},{"issue":"2","key":"18_CR19","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"issue":"1","key":"18_CR20","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/s10472-010-9208-8","volume":"59","author":"M Leuschel","year":"2010","unstructured":"Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. Ann. Math. Artif. Intell. 59(1), 81\u2013106 (2010)","journal-title":"Ann. Math. Artif. Intell."},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/978-3-642-10373-5_25","volume-title":"Formal Methods and Software Engineering","author":"PJ Matos","year":"2009","unstructured":"Matos, P.J., Fischer, B., Marques-Silva, J.: A lazy unbounded model checker for Event-B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 485\u2013503. Springer, Heidelberg (2009)"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Ph.D. thesis, Boston (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/978-3-662-46681-0_58","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Moln\u00e1r","year":"2015","unstructured":"Moln\u00e1r, V., Darvas, D., V\u00f6r\u00f6s, A., Bartha, T.: Saturation-based incremental LTL model checking with inductive proofs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 643\u2013657. Springer, Heidelberg (2015)"},{"key":"18_CR25","unstructured":"de Moura, L., Owre, S., Shankar, N.: The SAL language manual. Technical report, SRI International, technical Report SRI-CSL-01-02 (Rev. 2) (2003)"},{"key":"18_CR26","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"11","author":"D Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9\u201321 (2010)","journal-title":"STTT"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of petri nets. In: Proceedings ATPN, pp. 374\u2013391 (1995)","DOI":"10.1007\/3-540-60029-9_50"},{"issue":"4","key":"18_CR28","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Asp. Comput."},{"issue":"11","key":"18_CR29","doi-asserted-by":"crossref","first-page":"2651","DOI":"10.1002\/nme.1620281111","volume":"28","author":"SW Sloan","year":"1989","unstructured":"Sloan, S.W.: A FORTRAN program for profile and wavefront reduction. Int. J. Numer. Meth. Eng. 28(11), 2651\u20132679 (1989)","journal-title":"Int. J. Numer. Meth. Eng."},{"key":"18_CR30","unstructured":"Whitefield, J.: Linking ProB and LTSmin (2015), Final Year Dissertation, University of Surrey"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-34032-1_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"K Winter","year":"2012","unstructured":"Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246\u2013260. Springer, Heidelberg (2012)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T18:33:20Z","timestamp":1567967600000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}