{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:46Z","timestamp":1771888186676,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"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_18","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T01:26:02Z","timestamp":1180315562000},"page":"350-369","source":"Crossref","is-referenced-by-count":6,"title":["Type Synthesis in B and the Translation of B to PVS"],"prefix":"10.1007","author":[{"given":"Jean-Paul","family":"Bodeveix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"18_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":"18_CR2","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Translating specifications in VDM-SL to PVS","author":"S. Agerholm","year":"1996","unstructured":"Agerholm, S. Translating specifications in VDM-SL to PVS. In J. Grundy J. VonWright and J. Harisson, editors, Proceeding of the 9th International Conference On Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 1\u201316, Turku, Finland, 1996. Springer-Verlag."},{"key":"18_CR3","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u0144oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual \u2014 Version V6.1. Technical Report 0203, INRIA, August 1997. http:\/\/coq.inria.fr ."},{"key":"18_CR4","unstructured":"J.-P. Bodeveix, M. Filali, and C. Munoz. A formalization of the B method in Coq and PVS. In FM\u201999-B Users Group Meeting \u2014 Applying B in an industrial context: Tools, Lessons and Techniques, pages 32\u201348, 1999."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"J. Bowen and M. Gordon. Z and HOL. In 8th Z User Meeting (ZUM\u201994). BCS FACS, June 1994.","DOI":"10.1007\/978-1-4471-3452-7_9"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 238\u2013252, Los Angeles, California, 1977. ACM Press, New York, NY.","DOI":"10.1145\/512950.512973"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"P. Chartier. Formalisation of B in Isabelle\/HOL. In Proc. Second B International Conference, Montpellier, France, 1998.","DOI":"10.1007\/BFb0053356"},{"key":"18_CR8","unstructured":"S. Crow, S. Owre, J. Rushby, N. Shankar, and S. Mandayam. A Tutorial Introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, http:\/\/www.csl.sri.com\/pvs , April 1995."},{"key":"18_CR9","unstructured":"P. Cousot. Abstract interpretation: Achievements and perspectives. In Proceedings of the SSGRR 2000 Computer & eBusiness International Conference, Compact disk paper 224 and electronic proceedings http:\/\/www.ssgrr.it\/en\/ssgrr2000\/proceedings.htm , L\u2019\u2019Aquila, Italy, July 31-August 6 2000. Scuola Superiore G. Reiss Romoli."},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44525-0_8","volume-title":"ZB\u20192000: Formal Specification and Development in Z and B","author":"T. Dimitrakos","year":"2000","unstructured":"T. Dimitrakos, J. Bicarregui, B. Matthews, and Maibaum. Compositional structuring in the B-method: A logical viewpoint of the static context. In J.-P. Bowen, S. Dunne, A. Galloway, and S. King, editors, ZB\u20192000: Formal Specification and Development in Z and B, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, September 2000."},{"key":"18_CR11","unstructured":"C. Dubois and V. Donzeau-Gouge. A step towards the mechanization of partial functions: domains as inductive predicates. In In Workshop on mechanization of partial functions, CADE 15, July 1998."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Reasoning inductively about Z specifications via unification","author":"D. Duffy","year":"2000","unstructured":"D. Duffy and I. Toyn. Reasoning inductively about Z specifications via unification. In Proceedings International Conference of Z and B Users, ZB2000, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, May 2000."},{"key":"18_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Typechecking Z","author":"D. Duffy","year":"2000","unstructured":"D. Duffy and I. Toyn. Typechecking Z. In Proceedings International Conference of Z and B Users, ZB2000, volume 1878 of Lecture Notes in Computer Science. Springer-Verlag, May 2000."},{"key":"18_CR14","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL . Cambridge University Press, 1994."},{"key":"18_CR15","unstructured":"M.J.C. Gordon. Merging hol with set theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, 1994."},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","first-page":"355","volume-title":"ZUM\u201995: The Z formal specification notation","author":"I. Kraan","year":"1995","unstructured":"I. Kraan and P. Baumann. Implementing Z in Isabelle. In Bowen and Hinchey, editors, ZUM\u201995: The Z formal specification notation, number 967 in Lecture Notes in Computer Science, pages 355\u2013373. Springer-Verlag, 1995."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","first-page":"283","volume-title":"A structure preserving encoding of Z in Isabelle\/HOL","author":"K. T. Santen","year":"1996","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics \u2014 9th International Conference, volume 1125of Lecture Notes in Computer Science, pages 283\u2013298. Springer Verlag, 1996."},{"key":"18_CR18","unstructured":"G Mariano. The Bcaml project. Technical report, INRETS, http:\/\/www3.inrets.fr\/Public\/ESTAS\/Mariano .Georges, 2001."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"S. Maharaj and J. Bicarregui. On verification of VDM specification and refinement with PVS. In proceedings of the 12th IEEE International Conference in Automated Software Engineering, pages 280\u2013289, 1997.","DOI":"10.1109\/ASE.1997.632849"},{"issue":"10","key":"18_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/comjnl\/40.10.640","volume":"40","author":"O. M\u00fcller","year":"1997","unstructured":"O. M\u00fcller and K. Slind. Treating partiality in a logic of total functions. The Computer Journal, 40(10):1\u201312, 1997.","journal-title":"The Computer Journal"},{"key":"18_CR21","unstructured":"L.C. Paulson. Introduction to Isabelle. Technical report, Computer laboratory, university of Cambrige, 1992."},{"issue":"3","key":"18_CR22","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353\u2013389, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/BFb0053355","volume-title":"Composition and refinement in the Bmethod","author":"M.-L. Potet","year":"1998","unstructured":"M.-L. Potet and Y. Rouzaud. Composition and refinement in the Bmethod. volume 1393 of Lecture Notes in Computer Science, pages 46\u201365. Springer-Verlag, 1998."},{"key":"18_CR24","series-title":"Lect Notes Comput Sci","volume-title":"HOLCF: Higher Order Logic of Computable Functions","author":"F. Regensburger","year":"1995","unstructured":"F. Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, number 971 in Lecture Notes in Computer Science, Aspen Grove, Utah, 1995. Springer-Verlag."},{"key":"18_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-48119-2_24","volume-title":"FM\u201999","author":"Y. Rouzaud","year":"1999","unstructured":"Y. Rouzaud. Interpreting the B-method in the refinement calculus. In J. Wing, J. Woodcock, and J. Davies, editors, FM\u201999, volume 1708 of Lecture Notes in Computer Science, pages 411\u2013430. Springer-Verlag, Sep 1999."}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T08:01:40Z","timestamp":1587542500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}