{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:53Z","timestamp":1725540533485},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_25","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T06:45:27Z","timestamp":1258353927000},"page":"485-503","source":"Crossref","is-referenced-by-count":6,"title":["A Lazy Unbounded Model Checker for Event-B"],"prefix":"10.1007","author":[{"given":"Paulo J.","family":"Matos","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Fischer","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/11415787_6","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"G. Smith","year":"2005","unstructured":"Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 85\u2013103. Springer, Heidelberg (2005)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1007\/11901433_37","volume-title":"Formal Methods and Software Engineering","author":"J. Derrick","year":"2006","unstructured":"Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 678\u2013696. Springer, Heidelberg (2006)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a05238, pp. 280\u2013293. Springer, Heidelberg (2008)"},{"key":"25_CR4","volume-title":"Communicating Sequential Processes","author":"C.A. Hoare","year":"1986","unstructured":"Hoare, C.A.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"25_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: M\u00e9t\u00e9or: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: Systems and Software Engineering. To be published by Cambridge University Press (2009)","DOI":"10.1017\/CBO9781139195881"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-87603-8_11","volume-title":"Abstract State Machines, B and Z","author":"S. Hallerstede","year":"2008","unstructured":"Hallerstede, S.: On the purpose of Event-B proof obligations. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 125\u2013138. Springer, Heidelberg (2008)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11955757_7","volume-title":"B 2007: Formal Specification and Development in B","author":"S. Hallerstede","year":"2006","unstructured":"Hallerstede, S.: Justifications for the Event-B modelling notation. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 49\u201363. Springer, Heidelberg (2006)"},{"key":"25_CR11","unstructured":"M\u00e9tayer, C., Voisin, L.: The Event-B mathematical language (March 2009), http:\/\/wiki.event-b.org\/index.php\/Event-B_Mathematical_Language"},{"key":"25_CR12","unstructured":"Flatt, M., et al.: Reference: PLT Scheme. Reference Manual PLT-TR2009-reference-v4.2, PLT Scheme Inc. (June 2009)"},{"key":"25_CR13","first-page":"236","volume-title":"Proc. Conf. on Programming Language Design and Implementation, SIGPLAN Notices","author":"M. Flatt","year":"1998","unstructured":"Flatt, M., Felleisen, M.: Units: Cool modules for hot languages. In: Proc. Conf. on Programming Language Design and Implementation, SIGPLAN Notices, vol.\u00a033(5), pp. 236\u2013248. ACM, New York (1998)"},{"key":"25_CR14","volume-title":"The B-method \u2014 an introduction","author":"S. Schneider","year":"2001","unstructured":"Schneider, S.: The B-method \u2014 an introduction. Palgrave Macmillan, Basingstoke (2001)"},{"key":"25_CR15","unstructured":"Colley, J.: An Investigation into using Event-B for sub-system development in a SystemC TLM flow. Private Communication (July 2007)"},{"key":"25_CR16","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"25_CR18","unstructured":"Leuschel, M., Plagge, D.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Technical Report STUPS\/2007\/02, Institut f\u00fcr Informatik, Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2007)"},{"key":"25_CR19","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/TASE.2008.33","volume-title":"Proc. 2nd Intl. Symposium on Theoretical Aspects of Software Engineering","author":"C. Spermann","year":"2008","unstructured":"Spermann, C., Leuschel, M.: ProB gets nauty: Effective symmetry reduction for B and Z models. In: Proc. 2nd Intl. Symposium on Theoretical Aspects of Software Engineering, pp. 15\u201322. IEEE, Los Alamitos (2008)"},{"key":"25_CR20","unstructured":"Plagge, D., Leuschel, M., Lopatkin, I., Iliasov, A., Romanovsky, A.: SAL, Kodkod, and BDDs for validation of B models. lessons and outlook. In: Proc. 4th Workshop on Automated Formal Methods (June 2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:54:55Z","timestamp":1606168495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}