{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:29Z","timestamp":1725664829952},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_17","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:28:31Z","timestamp":1330298911000},"page":"318-337","source":"Crossref","is-referenced-by-count":28,"title":["A corrected failure-divergence model for CSP in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"H.","family":"Tej","sequence":"first","affiliation":[]},{"given":"B.","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"17_CR1","unstructured":"P.B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, 1986."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"J. P. Bowen,M. J. Hinchey: Seven more Myths of Formal Methods: Dispelling Industrial Prejudices, in FME'94: Industrial Benefit of Formal Methods, proc. 2nd Int. Symposium of Formal Methods Europe, LNCS 873, Springer Verlag 1994, pp. 105\u2013117.","DOI":"10.1007\/3-540-58555-9_91"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"S.D. Brookes, A.W. Roscoe: An improved failures model for communicating processes. In: S.D.Brookes (ed.): Seminar on Semantics of Concurrency. LNCS 197, Springer Verlag, pp. 281\u2013305. 1985.","DOI":"10.1007\/3-540-15670-4_14"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"A.J. Camillieri: A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics. G. Birtwistle (ed): IVth Higher Order Workshop, Banff 1990. Workshops in Computing, Springer Verlag, 1991.","DOI":"10.1007\/978-1-4471-3182-3_9"},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church: A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940, pp. 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"17_CR6","unstructured":"C. Fischer: Combining CSP and Z. Submitted for publication."},{"key":"17_CR7","unstructured":"Formal Systems (Europe) Ltd: Failures-Divergence Refinement: FDR2, Dec. 1995. Preliminary Manual."},{"key":"17_CR8","unstructured":"M.J.C. Gordon,T.M. Melham: Introduction to HOL: a Theorem Proving Environment for Higher order Logics, Cambridge Univ. Press, 1993."},{"key":"17_CR9","unstructured":"C.A.R.Hoare: Communication Sequential Processes.Prentice-Hall, 1985"},{"key":"17_CR10","unstructured":"Kolyang, C. L\u00fcth, T. Meier, B. Wolff: Generic Interfaces for Formal Development Support Tools. In: Workshop for Verification and Validation Tools, Bremen. to appear in LNCS."},{"key":"17_CR11","unstructured":"B. Krieg-Bruckner, J. Peleska, E.-R. Olderog, D. Balzer, A. Baer,: Uniform Workbench-Universelle Entwicklungsumgebung f\u00fcr formale Methoden. Technischer Bericht 8\/95, Universitdt Bremen, 1995. See also the project home-page: http:\/\/www.informatik.unibremen.de\/uniform."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Kolyang, T. Santen, B. Wolff: 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":"17_CR13","unstructured":"Kolyang, T. Santen, B. Wolff: A structure preserving encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy and J. Harrison (eds): Theorem Proving in Higher\/Order Logics-9th International Conference, LNCS 1125, pp. 283\u2013298, 1996."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"L. C. Paulson: Isabelle-A Generic Theorem Prover. LNCS 828, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"17_CR15","unstructured":"A.W. Roscoe, G. Barett: Unbounded Nondeterminism in CSP. In: M. Main, A.Melton,M.Mislove,D.Schmidt (eds): 9th International Conference in Mathematical Foundations of Programming Semantics. LNCS 442,pp. 160\u2013193, 1989."},{"key":"17_CR16","unstructured":"F. Regensburger: HOLCF: Eine konservative Einbettung von LCF in HOL. Phd thesis, Technische Universit\u00e4t M\u00fcnchen. 1994."},{"key":"17_CR17","unstructured":"A.W. Roscoe: An alternative Order for the Failures Model. In: Two Papers on CSP. Technical Monograph PRG-67, Oxford university Computer Laboratory, Programming Research Group, July 1988."},{"key":"17_CR18","unstructured":"A.W. Roscoe, e-mail communication with the authors."}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:46Z","timestamp":1605647926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}