{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:14:32Z","timestamp":1725484472566},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000297"},{"type":"electronic","value":"9783540361039"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36103-0_15","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T23:15:07Z","timestamp":1179270907000},"page":"120-131","source":"Crossref","is-referenced-by-count":1,"title":["Mechanization of an Integrated Approach: Shallow Embedding into SAL\/PVS"],"prefix":"10.1007","author":[{"given":"J. Christian","family":"Attiogb\u00e9","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,10]]},"reference":[{"key":"15_CR1","unstructured":"A. W. Gravell and C. H. Pratten. Embedding a Formal Notation: Experiences of Automating the Embedding of Z in the Higher Order Logic of PVS and HOL. In M. Newey, editor. Supplementary Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics: Emerging Trends,(TPHOL\u201998). Australian National University [16], pages 73\u201384, 1998."},{"key":"15_CR2","unstructured":"C. Attiogb\u00e9. Configuration Machines: A Simple Formalism For Specifying Multifaceted Systems. Technical Report 181, IRIN, University of Nantes, 1998."},{"key":"15_CR3","unstructured":"C. Attiogb\u00e9. The Access Control System: Specification with Configuration Machines. In Proc. of AFADL\u20192000, pages 203\u2013220, France, 2000."},{"key":"15_CR4","unstructured":"C. Attiogb\u00e9. Mechanization of Configuration Machines: Shallow Embedding into SAL\/PVS. Technical Report 01.8, IRIN, University of Nantes, 2001."},{"key":"15_CR5","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, 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. Michael Holloway, editor, Proc. of the Fifth NASA Langley Formal Methods Workshop (LFM\u20192000), pages 187\u2013196, Vancouver, 2000."},{"key":"15_CR6","unstructured":"R. Boulton, A. Gorgon, M.J.C. Gordon, J. Hebert, and J. van Tassel. Experience with Embedding Hardware Description Language in HOL. In Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129\u2013156, North-Holland, 1992. IFIP TC10\/WG 10.2."},{"issue":"5\u20136","key":"15_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J. P. Bowen","year":"1995","unstructured":"J. P. Bowen and M. J. C. Gordon. A Shallow Embedding of Z in HOL. Information and Software Technology, 37(5\u20136):269\u2013276, 1995.","journal-title":"Information and Software Technology"},{"key":"15_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the International Conference on Formal Methods (FM\u201999)","author":"M. Bozga","year":"1999","unstructured":"M. Bozga, J. C. Ferandez, L. Ghirvu, S. Graph, J. P. Krimm, and L. Mounier. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In J. Wing and J. Woodcock and J. Davies, editor, Proc. of the International Conference on Formal Methods (FM\u201999), volume 1708 of Lecture Notes in Computer Science, France, 1999. Springer-Verlag."},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01214622","volume":"7","author":"M. J. Butler","year":"1995","unstructured":"M. J. Butler and C. C. Morgan. Action Systems, Unbounded Nondeterminism, and Infinite Traces. Formal Aspects of Computing, 7:37\u201353, 1995.","journal-title":"Formal Aspects of Computing"},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Proc. of Computer-Aided Verification (CAV\u201996)","author":"D. L. Dill","year":"1996","unstructured":"D. L. Dill. The Mur\u00f8 Verification System. In Proc. of Computer-Aided Verification (CAV\u201996), volume 1102 of Lecture Notes in Computer Science, pages 390\u2013393, New Jersey, USA, 1996. Springer-Verlag."},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Proc. of the 8th Conference on Computer-Aided Verification (CAV\u201996)","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In R. Alur and T. A. Henzinger, editors, Proc. of the 8th Conference on Computer-Aided Verification (CAV\u201996), volume 1102 of Lecture Notes in Computer Science, pages 437\u2013440. Springer-Verlag, 1996."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"C. Fischer. CSP-OZ: A Combination of Object-Z and CSP. In H. Bowmann and J. Derick, editors, Proc. of FMOODS\u201997, volume 2, pages 423\u2013438. Chapman and Hall, 1997.","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"15_CR13","unstructured":"A. Galloway. Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi-Perspectives Systems. PhD thesis, University of Teesside-School of Computing and Mathematics, 1996."},{"key":"15_CR14","unstructured":"M.J.C. Gordon. Introduction to HOL: A Theorem Proving Environment. Cambridge University Press, 1993."},{"key":"15_CR15","unstructured":"J. Crow and S. Owre and J. Rushby and N. Shankar and M. Srivas. A Tutorial Introduction to PVS. In Proc. of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT\u201995). IEEE Press, 1995. Florida."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"J. Grundy and M. Newey, editor. Supplementary Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics: Emerging Trends, (TPHOL\u201998). Australian National University, 1998.","DOI":"10.1007\/BFb0055125"},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Proc. of the International Conference on Theorem Proving in Higher Order Logic (TPHOL\u201996)","author":"Kolyang","year":"1996","unstructured":"Kolyang, T Santen, and B. Wolff. A Structure Preserving Encoding of Z in Isabelle\/HOL. In Proc. of the International Conference on Theorem Proving in Higher Order Logic (TPHOL\u201996), volume 1125 of Lecture Notes in Computer Science, pages 283\u2013298. Springer-Verlag, 1996."},{"key":"15_CR18","series-title":"Lect Notes Comput Sci","first-page":"1187","volume-title":"Proc. of the International Conference on Formal Methods (FM\u201999)","author":"B. Krieg-Br\u00fcckner","year":"1999","unstructured":"B. Krieg-Br\u00fcckner, J. Peleska, E. R. Olderog, and A. Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. In J. Wing and J. Woodcock and J. Davies, editor, Proc. of the International Conference on Formal Methods (FM\u201999), volume 1708 of Lecture Notes in Computer Science, pages 1187\u20131205, France, 1999. Springer-Verlag."},{"key":"15_CR19","unstructured":"A. Martin. Approaches to proof in Z. Technical report, University of Southampton, 1997."},{"key":"15_CR20","unstructured":"C. Mu\u00f1oz. Specification of the Flight Guidance System in (unofficial) SAL. Technical report, ICASE, http:\/\/www.icase.edu\/~munoz\/SAL\/sal.html , 1999."},{"key":"15_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/3-540-48119-2_26","volume-title":"Proc. of the World Congress in Formal Methods (FM99)","author":"C. Mu\u00f1oz","year":"1999","unstructured":"C. Mu\u00f1oz and J. Rushby. Structural Embeddings: Mechanization with Method. In J. Wing and J. Woodcock, editor, Proc. of the World Congress in Formal Methods (FM99), volume 1708 of Lecture Notes in Computer Science, pages 452\u2013471, France, 1999. Springer-Verlag."},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"D. Park, U. Stern, J. U. Skakkebaek, and D. L. Dill. Java Model Checking. In Proc. of the Fifteenth IEEE International Conference on Automated Software Engineering (ASE\u20192000), pages 253\u2013256, 2000.","DOI":"10.1109\/ASE.2000.873671"},{"key":"15_CR23","unstructured":"R. B\u00fcssow, R. Geisler, W. Grieskamp and M. Klar. The \u03bc SZ Notation, Version 1.0. Technical report, Teschnische Universit\u00e4t Berlin, Fachbereich Informatik, December 1997."},{"key":"15_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-44518-8_16","volume-title":"Proc. of the Workshop on Abstract State Machines: Theory and Applications (ASM\u20192000)","author":"N. Shankar","year":"2000","unstructured":"N. Shankar. Symbolic Analysis of Transition Systems. In Y. Gurevich, P. W. Kutter, M. Odersky, and L. Thiele, editors, Proc. of the Workshop on Abstract State Machines: Theory and Applications (ASM\u20192000), volume 1912 of Lecture Notes in Computer Science, pages 287\u2013302, Switzerland, 2000. Springer-Verlag."},{"key":"15_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1007\/BFb0027281","volume-title":"Proc. ZUM\u201997","author":"W.J. Stoddart","year":"1997","unstructured":"W.J. Stoddart. An Introduction to the Event Calculus. In Proc. ZUM\u201997, volume 1212 of Lecture Notes in Computer Science, pages 10\u201334. Springer-Verlag, 1997."},{"key":"15_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/3-540-63533-5_30","volume-title":"Proc. of Formal Methods: Their Industrial Application and Strengthened Foundations (FME\u2019 97)","author":"D. W. J. Stringer-Calvert","year":"1997","unstructured":"D. W. J. Stringer-Calvert, S. Stepney, and I. Wand. Using PVS to Prove a Z Refinement: A Case Study. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, Proc. of Formal Methods: Their Industrial Application and Strengthened Foundations (FME\u2019 97), volume 1313 of Lecture Notes in Computer Science, pages 573\u2013588, Austria, 1997. Springer-Verlag."},{"key":"15_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/3-540-59293-8_237","volume-title":"Proc. of Theory and Practice of Software Development","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and the STeP group. STeP: The Stanford Temporal Prover. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proc. of Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 793\u2013794. Springer-Verlag, 1995."},{"key":"15_CR28","unstructured":"ITU Recommendation Z.100. Specification and Description Language SDL. Technical report, ITU, 1994."},{"key":"15_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"Proc. of The Z Users Meeting (ZUM\u201998)","author":"C. Fischer","year":"1998","unstructured":"C. Fischer. How to combine Z with a Process Algebra. In J. P. Bowen, A. Fett, et M. G. Hinchey, \u00e9diteurs, Proc. of The Z Users Meeting (ZUM\u201998), volume 1493 of Lecture Notes in Computer Science, pages 5\u201323. Springer-Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36103-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:56:15Z","timestamp":1556398575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36103-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000297","9783540361039"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-36103-0_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}