{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:29:05Z","timestamp":1743074945550,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_30","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"513-527","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Extending B with Control Flow Breaks"],"prefix":"10.1007","author":[{"given":"Lilian","family":"Burdy","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Requet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Jean-Raymond Abrial. The B Book, Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"30_CR2","unstructured":"Lilian Burdy and Antoine Requet. Jack: Java Applet Correctness Kit. In GDC 2002, Singapore, November 2002."},{"key":"30_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-45614-7_17","volume-title":"Formal Methods \u2014 Getting IT Right","author":"L. Casset","year":"2002","unstructured":"Ludovic Casset. Development of an Embedded Verifier for Java Card Byte Code using Formal Methods. In Lars-Henrik Eriksson and Peter Alexander Lindsay, editors, Formal Methods \u2014 Getting IT Right, volume 2391 of Lecture Notes in Computer Science, pages 290\u2013309. Springer-Verlag, July 22\u201324 2002."},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Ludovic Casset, Lilian Burdy, and Antoine Requet. Formal Development of an Embedded Verifier for Java Card Byte Code. In DSN 2002, International Conference on Dependable Systems & Networks, pages 51\u201356, Washington, D.C., USA, June 2002.","DOI":"10.1109\/DSN.2002.1028886"},{"key":"30_CR5","volume-title":"Java Program Verification in Higher-Order Logic with PVS and Isabelle","author":"M. Huisman","year":"2001","unstructured":"Marieke Huisman. Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, The Netherlands, 2001."},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Marieke Huisman and Bart Jacobs. Java Program Verification via a Hoare Logic with Abrupt Termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering (FASE), volume 1783, pages 284\u2013303. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-46428-X_20"},{"key":"30_CR7","unstructured":"Pierre Lartigue and Denis Sabatier. The use of the B formal method for the design and the validation of the transaction mechanism for smart card applications. In Formal Methods in System Design, Special Issue on FM\u201999, November 1999."},{"key":"30_CR8","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume":"2031","author":"J. van den Berg","year":"2001","unstructured":"Joachim van den Berg and Bart Jacobs. The LOOP Compiler for Java and JML. Lecture Notes in Computer Science, 2031:299\u2013312, 2001.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:03:57Z","timestamp":1737173037000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}