{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T11:23:04Z","timestamp":1768303384469,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540431664","type":"print"},{"value":"9783540456483","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_8","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T05:26:02Z","timestamp":1180329962000},"page":"140-161","source":"Crossref","is-referenced-by-count":11,"title":["An Approach to Combining B and Alloy"],"prefix":"10.1007","author":[{"given":"Leonid","family":"Mikhailov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"8_CR2","unstructured":"B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual., 1999. Available at http:\/\/www.b-core.com\/ONLINEDOC\/Contents.html ."},{"key":"8_CR3","unstructured":"S. Bensalem, C. Mu\u00f1oz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In C. M. Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187\u2013196, Hampton, VA, June 2000. NASA Langley Research Center."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"J. C. Bicarregui and B. M. Matthews. Proof and refutation in formal software development. In 3rd Irish Workshop on Formal Software Development, http:\/\/www.ewic.org.uk , July 1999. British Computer Society, Electornic Workshops in Computing.","DOI":"10.14236\/ewic\/IWFM1999.1"},{"key":"8_CR5","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 user manual, October 1997. Available at http:\/\/www.formal.demon.co.uk ."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"M. Gordon. Introduction to the HOL system. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedigns of the International Workshop on the HOL Theorem Proving System and its Applications, pages 2\u20133, Los Alamitos, CA, USA, Aug. 1992. IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596265"},{"issue":"5","key":"8_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker spin. IEEE Trans. on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"8_CR8","unstructured":"D. Jackson. Alloy: A lightweight object modelling notation. MIT Lab for Computer Science, July 2000."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyser. In Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337616"},{"key":"8_CR10","unstructured":"K. MacMillan. The SMV Language. Cadence Berkeley Labs, 1999."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"8_CR12","unstructured":"L. Mikhailov and M. Butler. Combining B and Alloy. In Proceedings of FMICS\u20192001, pages 29\u201345, Paris, July 2001. INRIA."},{"key":"8_CR13","first-page":"357","volume-title":"PVS Tutorial","author":"N. Shankar","year":"1993","unstructured":"N. Shankar and J. M. Rushby. PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993. Also appears in Tutorial Notes, Formal Methods Europe\u2019 93: Industrial-Strength Formal Methods, pages 357\u2013406, Odense, Denmark, April 1993."},{"key":"8_CR14","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1987."},{"key":"8_CR15","unstructured":"M. Woodman and B. Heal. Introduction to VDM. McGraw-Hill, 1993. ISBN 0-07-707434-3."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:34:55Z","timestamp":1737052495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}