{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:36:57Z","timestamp":1725543417693},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642114465"},{"type":"electronic","value":"9783642114472"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-11447-2_6","type":"book-chapter","created":{"date-parts":[[2010,1,8]],"date-time":"2010-01-08T14:47:12Z","timestamp":1262962032000},"page":"78-92","source":"Crossref","is-referenced-by-count":3,"title":["Validating and Animating Higher-Order Recursive Functions in B"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Cansell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/3-540-45648-1_19","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2002","unstructured":"Abrial, J.-R., Cansell, D., Laffitte, G.: Higher-order mathematics in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 370\u2013393. Springer, Heidelberg (2002)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45648-1_13","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 242\u2013269. Springer, Heidelberg (2002)"},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1023\/A:1016503426126","volume":"6","author":"M. Butler","year":"2002","unstructured":"Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Design Automation for Embedded Systems\u00a06(4), 355\u2013366 (2002)","journal-title":"Design Automation for Embedded Systems"},{"issue":"3\u20134","key":"6_CR5","first-page":"221","volume":"22","author":"D. Cansell","year":"2003","unstructured":"Cansell, D., M\u00e9ry, D.: Foundations of the B method. Computing and informatics\u00a022(3\u20134), 221\u2013256 (2003)","journal-title":"Computing and informatics"},{"key":"6_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"6_CR7","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"6_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"6_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":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11576280_24","volume-title":"Formal Methods and Software Engineering","author":"M. Leuschel","year":"2005","unstructured":"Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 345\u2013359. Springer, Heidelberg (2005)"},{"issue":"1","key":"6_CR11","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF01211317","volume":"5","author":"T. Massart","year":"1993","unstructured":"Massart, T., Devillers, R.: Equality of agent expressions is preserved under an extension of the universe of actions. Formal Aspects of Computing\u00a05(1), 79\u201388 (1993)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"issue":"2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/571535.571570","volume":"31","author":"J.S. Robertson","year":"1999","unstructured":"Robertson, J.S.: How many recursive calls does a recursive function make? SIGCSE Bull.\u00a031(2), 60\u201361 (1999)","journal-title":"SIGCSE Bull."},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-44525-0_7","volume-title":"ZB 2000: Formal Specification and Development in Z and B","author":"K. Robinson","year":"2000","unstructured":"Robinson, K.: Reconciling axiomatic and model-based specifications using the B method. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol.\u00a01878, pp. 95\u2013106. Springer, Heidelberg (2000)"},{"key":"6_CR15","volume-title":"Concepts, Techniques, and Models of Computer Programming","author":"P.V. Roy","year":"2004","unstructured":"Roy, P.V., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004)"}],"container-title":["Lecture Notes in Computer Science","Rigorous Methods for Software Construction and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11447-2_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:52:22Z","timestamp":1619783542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11447-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642114465","9783642114472"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11447-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}