{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:21Z","timestamp":1763467761486},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_25","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T18:32:59Z","timestamp":1161109979000},"page":"362-376","source":"Crossref","is-referenced-by-count":20,"title":["Verification Condition Generation Via Theorem Proving"],"prefix":"10.1007","author":[{"given":"John","family":"Matthews","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandip","family":"Ray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","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":"25_CR2","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":"25_CR3","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning Meanings to Programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematcs, Providence, Rhode Island, vol.\u00a0XIX, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"25_CR4","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":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-30494-4_6","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Ray","year":"2004","unstructured":"Ray, S., Moore, J.S.: Proof Styles in Operational Semantics. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 67\u201381. Springer, Heidelberg (2004)"},{"key":"25_CR6","first-page":"119","volume":"3","author":"Z. Manna","year":"1969","unstructured":"Manna, Z.: The Correctness of Programs. JCSS\u00a03, 119\u2013127 (1969)","journal-title":"JCSS"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the java specification: Proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, pp. 119\u2013156. Springer, Heidelberg (1999)"},{"key":"25_CR8","first-page":"89","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"D. Greve","year":"2000","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-Speed, Analyzable Simulators. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, pp. 89\u2013106. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"25_CR9","series-title":"NATO ASI Series F: Computer and Systems Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/978-3-642-60858-2_26","volume-title":"Mathematical Methods in Program Development","author":"N. Shankar","year":"1997","unstructured":"Shankar, N.: Machine-Assisted Verification Using Theorem Proving and Model Checking. In: Broy, M., Schieder, B. (eds.) Mathematical Methods in Program Development. NATO ASI Series F: Computer and Systems Science, vol.\u00a0158, pp. 499\u2013528. Springer, Heidelberg (1997)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A Certifying Compiler for Java. In: ACM SIGPLAN 2000 conference on Programming language design and implementation, pp. 95\u2013107 (2000)","DOI":"10.1145\/349299.349315"},{"key":"25_CR11","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)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher Order Logics","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Moore, J.S.: Partial Functions in ACL2. Journal of Automated Reasoning\u00a031, 107\u2013127 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR14","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/B978-0-12-450010-5.50007-4","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"R.S. Boyer","year":"1991","unstructured":"Boyer, R.S., Goldshlag, D., Kaufmann, M., Moore, J.S.: Functional Instantiation in First Order Logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7\u201326. Academic Press, London (1991)"},{"key":"25_CR15","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":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/10930755_7","volume-title":"16th International Conference on Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2003","unstructured":"Slind, K., Hurd, J.: Applications of polytypism in theorem proving. In: Basin, D., Wolff, B. (eds.) TestCom 2004. LNCS, vol.\u00a02978, pp. 103\u2013119. Springer, Heidelberg (2003)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/11541868_21","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Toma","year":"2005","unstructured":"Toma, D., Borrione, D.: Formal verification of a SHA-1 circuit core using ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 326\u2013341. Springer, Heidelberg (2005)"},{"key":"25_CR18","volume-title":"Applied Cryptography: Protocols, Algorithms, and Source Code in C","author":"B. Schneier","year":"1995","unstructured":"Schneier, B.: Applied Cryptography: Protocols, Algorithms, and Source Code in C, 2nd edn. John Wiley, Chichester (1995)","edition":"2"},{"key":"25_CR19","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":"25_CR20","unstructured":"Yu, Y.: Automated Proofs of Object Code for a Widely Used Microprocessor. PhD thesis, University of Texas at Austin (1992)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 63\u201377. Springer, Heidelberg (2002)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-24721-0_17","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Hamon","year":"2004","unstructured":"Hamon, G., Rushby, J.: An Operational Semantics for Stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 229\u2013243. Springer, Heidelberg (2004)"},{"key":"25_CR23","volume-title":"Collected Works","author":"H.H. Goldstein","year":"1961","unstructured":"Goldstein, H.H., von Neumann, J.: Planning and Coding Problems for an Electronic Computing Instrument. In: von Neumann, J. (ed.) Collected Works, vol.\u00a0V, Pergamon Press, Oxford (1961)"},{"key":"25_CR24","unstructured":"Turing, A.M.: Checking a Large Routine. In: Report of a Conference on High Speed Automatic Calculating Machine, University Mathematical Laboratory, Cambridge, England, pp. 67\u201369 (1949)"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded Commands, Non-determinacy and a Calculus for Derivation of Programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"25_CR26","unstructured":"King, J.C.: A Program Verifier. PhD thesis, Carnegie-Melon University (1969)"},{"key":"25_CR27","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended Static Checking for Java. Technical Report 159, Compaq Systems Research Center (1998)"},{"key":"25_CR28","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1109\/32.879807","volume":"26","author":"S. King","year":"2000","unstructured":"King, S., Hammond, J., Chapman, R., Pryor, A.: Is Proof More Cost-Effective Than Testing? IEEE Transactions on Software Engineering\u00a026, 675\u2013686 (2000)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding Exponential Explosion: Generating Compact Verification Conditions. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 193\u2013205 (2001)","DOI":"10.1145\/360204.360220"},{"key":"25_CR30","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett.\u00a093, 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"25_CR31","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P. Homeier","year":"1995","unstructured":"Homeier, P., Martin, D.: A Mechanically Verified Verification Condition Generator. The Computer Journal\u00a038, 131\u2013141 (1995)","journal-title":"The Computer Journal"},{"key":"25_CR32","unstructured":"Gloess, P.Y.: Imperative Program Verification in PVS. Technical report, \u00c9cole Nationale Sup\u00e9rieure \u00c9lectronique, Informatique et Radiocommunications de bordeaux (1999)"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"25_CR34","unstructured":"Norrish, M.: C Formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving Pointer Programs in Higher-Order Logic. In: Baader, F. (ed.) CADE 2003. LNCS, vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"25_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11541868_17","volume-title":"Theorem Proving in Higher Order Logics","author":"V. Ortner","year":"2005","unstructured":"Ortner, V., Schirmer, N.: Verification of BDD normalization. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 261\u2013277. Springer, Heidelberg (2005)"},{"key":"25_CR37","unstructured":"Matthews, J., Vroon, D.: Partial Clock Functions in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) 5th ACL2 Workshop (2004)"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-Carrying Code. In: POPL 1997, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational Proof-Carrying Code. In: LICS\u00a02001, pp. 247\u2013258 (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"25_CR40","unstructured":"Greve, D., Richards, R., Wilding, M.: A Summary of Intrinsic Partitioning Verification. In: Kaufmann, M., Moore, J.S. (eds.) 5th ACL2 Workshop (2004)"},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"Hardin, D., Smith, E.W., Young, W.D.: A Robust Machine Code Proof Framework for Highly Secure Applications. In: Manolios, P., Wilding, M. (eds.) 6th ACL2 Workshop (2006)","DOI":"10.1145\/1217975.1217978"},{"key":"25_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/11541868_11","volume-title":"Theorem Proving in Higher Order Logics","author":"W.A. Hunt Jr.","year":"2005","unstructured":"Hunt Jr., W.A., Kaufmann, M., Krug, R.B., Moore, J.S., Smith, E.W.: Meta Reasoning in ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 163\u2013178. Springer, Heidelberg (2005)"},{"key":"25_CR43","doi-asserted-by":"crossref","unstructured":"Pike, L., Shields, M., Matthews, J.: A Verifying Core for a Cryptographic Language Compiler. In: Manolios, P., Wilding, M. (eds.) 6th ACL2 Workshop (2006)","DOI":"10.1145\/1217975.1217977"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11916277_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:42:22Z","timestamp":1619509342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/11916277_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}