{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:36:27Z","timestamp":1757313387680,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_3","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"24-38","source":"Crossref","is-referenced-by-count":23,"title":["Translating TLA\u2009+\u2009 to B for Validation with ProB"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Hansen","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14808-8_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\u2009+\u2009 Proof System: Building a Heterogeneous Verification Platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, p. 44. Springer, Heidelberg (2010)"},{"key":"3_CR3","unstructured":"ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009), http:\/\/www.atelierb.eu\/"},{"issue":"4-5","key":"3_CR4","first-page":"767","volume":"11","author":"S. Hallerstede","year":"2011","unstructured":"Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP\u00a011(4-5), 767\u2013782 (2011)","journal-title":"TPLP"},{"key":"3_CR5","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"3_CR6","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.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","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. Annals of Mathematics and Artificial Intelligence\u00a059(1), 81\u2013106 (2010)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"3_CR8","unstructured":"Merz, S.: TLA+ Case Study: A Resource Allocator. Technical Report A04-R-101, INRIA Lorraine - LORIA (2004), http:\/\/hal.inria.fr\/inria-00107809"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-28717-6_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Merz","year":"2012","unstructured":"Merz, S., Vanzetto, H.: Automatic Verification of TLA\u2009+\u2009 Proof Obligations with SMT Solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 289\u2013303. Springer, Heidelberg (2012)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-48242-3_7","volume-title":"Logic Programming and Automated Reasoning","author":"Y. Mokhtari","year":"1999","unstructured":"Mokhtari, Y., Merz, S.: Animating TLA Specifications. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705, pp. 92\u2013110. Springer, Heidelberg (1999)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Mosbahi, O., Jemni, L., Jaray, J.: A formal approach for the development of automated systems. In: Filipe, J., Shishkov, B., Helfert, M. (eds.) ICSOFT (SE), pp. 304\u2013310. INSTICC Press (2007)","DOI":"10.5220\/0001342503040310"},{"key":"3_CR12","doi-asserted-by":"publisher","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\u00a011, 9\u201321 (2010)","journal-title":"STTT"},{"key":"3_CR13","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\u2009+\u2009 Specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, 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-642-30729-4_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T18:21:52Z","timestamp":1743618112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}