{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:38Z","timestamp":1725631958966},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105411","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"283-298","source":"Crossref","is-referenced-by-count":41,"title":["A structure preserving encoding of Z in isabelle\/HOL"],"prefix":"10.1007","author":[{"family":"Kolyang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Santen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"19_CR1","unstructured":"Bowen, J. P., Gordon, M. J. C.: Z and HOL. In Bowen, J.P. and Hall, J.A. (ed.): Z Users Workshop, Cambridge 1994, Workshops in Computing, pp. 141\u2013167, Springer Verlag, 1994"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Dick, J., Faivre, A.: Automating the Generation and Sequencing of Test Cases from Model-Based Specifications. In Woodcock, Larsen (eds.), Proc. Formal Methods Europe, pp. 268\u2013284, LNCS 670, Springer Verlag, 1993.","DOI":"10.1007\/BFb0024651"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Ehrig, H. Mahr, B.: Fundamentals of Algebraic Specification: Volume 1: Equations and Initial Semantics, Springer Verlag, 1985","DOI":"10.1007\/978-3-642-69962-7"},{"key":"19_CR4","unstructured":"M. Engel, J.U.Skakkeb\u00e6k: Applying PVS to Z. ProCoS II document [ID\/DTU ME 3\/1], Technical University of Denmark. 1995."},{"key":"19_CR5","unstructured":"Gordon, M.J.C., Melham, T.M.: Introduction to HOL: a Theorem Proving Environment for Higher order Logics, Cambridge University Press, 1993."},{"key":"19_CR6","series-title":"Technical Report","volume-title":"Proof rules for Balzac","author":"W. T. Harwood","year":"1991","unstructured":"Harwood, W. T.: Proof rules for Balzac. Technical Report WTH\/P7\/001, Imperial Software Technology, Cambridge, UK, 1991."},{"key":"19_CR7","unstructured":"S. J\u00e4hnichen (director): ESPRESS \u2014 Engineering of safety-critical embedded systems. Online information available via http:\/\/www.first.gmd.de\/org\/espres.html."},{"issue":"1","key":"19_CR8","first-page":"10","volume":"1","author":"R. B. Jones","year":"1992","unstructured":"Jones, R. B.: ICL ProofPrower. BCS FACS FACTS Series III, 1(1):10\u201313, Winter 1992.","journal-title":"BCS FACS FACTS Series III"},{"key":"19_CR9","series-title":"Technical Report","volume-title":"The Z Syntax Supported by Balzac II\/1","author":"L. E. Jordan","year":"1991","unstructured":"Jordan, L. E.: The Z Syntax Supported by Balzac II\/1. Technical Report LEJ\/S1\/001. Imperial Software Technology, Cambridge, UK, 1991."},{"key":"19_CR10","unstructured":"Kraan, I., Baumann, P.: Implementing Z in Isabelle. In Bowen, Hinchey (eds.), ZUM\u2019 95: The Z Formal Specification Notation, pp. 355\u2013373, LNCS 967, Springer Verlag, 1995."},{"key":"19_CR11","unstructured":"Krieg-Br\u00fcckner, B., Peleska, J., Olderog, E.-R., Balzer, D., Baer, A.: Uniform Workbench \u2014 Universelle Entwicklungsumgebung f\u00fcr formale Methoden. Technischer Bericht 8\/95, Universit\u00e4t Bremen, 1995. Also available online via http:\/\/www.informatik.uni-bremen.de\/~uniform."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Kolyang, Santen, T., Wolff, B: Correct and User-Friendly Implementations of Transformation Systems. Proc. Formal Methods Europe, Oxford. LNCS 1051, Springer Verlag, 1996.","DOI":"10.1007\/3-540-60973-3_111"},{"key":"19_CR13","unstructured":"Maharaj, S.: Implementing Z in LEGO. Unpublished M.Sc. thesis. Department of Computer Science, University of Edinburgh, September 1990."},{"key":"19_CR14","unstructured":"Martin, A.: Machine-Assisted Theorem-Proving for Software Engineering, Unpublished PhD Thesis, University of Oxford, 1994."},{"key":"19_CR15","unstructured":"Meisels, I., Saaltink, M.Z.: The Z\/EVES Reference Manual (draft). Technical report TR-95-5493-03, ORA Canada, December 1995"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Nicholls, J. (ed., prepared by the members of the Z Standards Panel): Z-Notation. Version 1.2. ISO-Draft. Online: http:\/\/www.comlab.ox.ac.uk\/oucl\/users\/andrew.martin\/zstandard\/.14th September 1995.","DOI":"10.21236\/ADA388235"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: Isabelle \u2014 A Generic Theorem Prover. LNCS 828, Springer Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"1","key":"19_CR18","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P.J. Robinson","year":"1993","unstructured":"Robinson, P.J., Staples, J.: Formalizing a Hierarchical Structure of Practical Mathematical Reasoning. Journal of Logic and Computation 3 (1), pp. 47\u201361, 1993","journal-title":"Journal of Logic and Computation"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Saaltink, M.Z.: Z and EVES. In Nicholls, J.E. (ed.) Z User Workshop, York 1991, Workshops in Computing, pages 223\u2013242. Springer Verlag 1992","DOI":"10.1007\/978-1-4471-3203-5_11"},{"key":"19_CR20","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual (2nd Edition). Prentice Hall, 1992."},{"key":"19_CR21","unstructured":"Spivey, J.M.: The fuzz Manual, Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9 9AN, UK 2nd edition, 1992"},{"key":"19_CR22","unstructured":"Toyn, I., Hall, J.: Proving Conjectures using CADiZ. York Software Engineering Ltd., September 1995."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Woodcock, J.C.P., Brien, S.M.: W: A logic for Z. In Nicholls, J.E. (ed.) Z User Workshop, York 1991, Workshops in Computing, pp. 77\u201396. Springer Verlag 1992","DOI":"10.1007\/978-1-4471-3203-5_4"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:52:18Z","timestamp":1639608738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105411"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0105411","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}