{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:46:53Z","timestamp":1754398013882},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_6","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"67-81","source":"Crossref","is-referenced-by-count":10,"title":["Proof Styles in Operational Semantics"],"prefix":"10.1007","author":[{"given":"Sandip","family":"Ray","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","first-page":"21","volume-title":"Proceedings of the Information Processing Congress","author":"J. McCarthy","year":"1962","unstructured":"McCarthy, J.: Towards a Mathematical Science of Computation. In: Proceedings of the Information Processing Congress, vol.\u00a062, pp. 21\u201328. North-Holland, Amsterdam (1962)"},{"key":"6_CR2","first-page":"141","volume-title":"Automated Reasoning and Its Applications: Essays in Honor of Larry Wos","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Moore, J.S.: Mechanized Formal Reasoning about Programs and Computing Machines. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pp. 141\u2013176. MIT Press, Cambridge (1996)"},{"key":"6_CR3","first-page":"227","volume-title":"Models, Algebras, and Logic of Engineering Software","author":"J.S. Moore","year":"2003","unstructured":"Moore, J.S.: Proving Theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, pp. 227\u2013290. IOS Press, Amsterdam (2003)"},{"key":"6_CR4","unstructured":"Bevier, W.R.: A Verified Operating System Kernel. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (1987)"},{"key":"6_CR5","unstructured":"Young, W.D.: A Verified Code Generator for a Subset of Gypsy. Technical Report 33, Computational Logic Inc (1988)"},{"key":"6_CR6","unstructured":"Flatau, A.D.: A Verified Implementation of an Applicative Language with Dynamic Storage Allocation. PhD thesis (1992)"},{"volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","year":"1993","key":"6_CR7","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"6_CR9","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"6_CR10","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning\u00a026, 161\u2013203 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR12","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1975","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1975)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Liu, H., Moore, J.S.: Executable JVM Model for Analytical Reasoning: A Study. In: ACM SIGPLAN 2003 Workshop on Interpreters, Virtual Machines, and Emulators, San Diego, CA (2003)","DOI":"10.1145\/858570.858572"},{"key":"6_CR14","unstructured":"Wilding, M.: Robust Computer System Proofs in PVS. In: Holloway, C.M., Hayhurst, K.J. (eds.) Fourth NASA Langley Formal Methods Workshop. NASA Conference Publication, vol.\u00a03356 (1997)"},{"key":"6_CR15","series-title":"Mathematical Aspects of Computer Science","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematcs","author":"R. Floyd","year":"1967","unstructured":"Floyd, R.: Assigning Meanings to Programs. In: Proceedings of Symposia in Applied Mathematcs. Mathematical Aspects of Computer Science, vol.\u00a0XIX, pp. 19\u201332. American Mathematical Society, Providence, Rhode Island (1967)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM\u00a012, 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded Commands, Non-determinacy and a Calculus for Derivation of Programs. Language Hierarchies and Interfaces, 111\u2013124 (1975)","DOI":"10.1007\/3-540-07994-7_51"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-540-39724-3_27","volume-title":"Correct Hardware Design and Verification Methods","author":"J.S. Moore","year":"2003","unstructured":"Moore, J.S.: Inductive Assertions and Operational Semantics. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 289\u2013303. Springer, Heidelberg (2003)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-27813-9_3","volume-title":"Computer Aided Verification","author":"S. Ray","year":"2004","unstructured":"Ray, S., Hunt Jr., W.A.: Deductive Verification of Pipelined Machines Using First-Order Quantification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 31\u201343. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:26:01Z","timestamp":1558279561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}