{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:15Z","timestamp":1763467995023},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540407966"},{"type":"electronic","value":"9783540452133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45213-3_4","type":"book-chapter","created":{"date-parts":[[2010,9,4]],"date-time":"2010-09-04T01:44:48Z","timestamp":1283564688000},"page":"25-35","source":"Crossref","is-referenced-by-count":11,"title":["The Verifying Compiler: A Grand Challenge for Computing Research"],"prefix":"10.1007","author":[{"given":"Tony","family":"Hoare","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Gray, J.: What Next? A Dozen Information-technology Research Goals, MS-TR-50, Microsoft Research (June 1999)","DOI":"10.1145\/602382.602401"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/BFb0026441","volume-title":"Compiler Construction","author":"K.M. Leino","year":"1998","unstructured":"Leino, K.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol.\u00a01383, pp. 302\u2013305. Springer, Heidelberg (1998)"},{"key":"4_CR3","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/52.976937","volume":"19","author":"A. Hall","year":"2002","unstructured":"Hall, A., Chapman, R.: Correctness by Construction: Developing a Commercial Secure System. IEEE Software\u00a019(1), 18\u201325 (2002)","journal-title":"IEEE Software"},{"key":"4_CR5","unstructured":"Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: USENIX Annual Technical Conference, Monterey, CA (June 2002)"},{"key":"4_CR6","unstructured":"See http:\/\/www.fbi.gov\/congress\/congress02\/nipc072402.htm a congressional statement presented by the director of the National Infrastructure Protection Center"},{"key":"4_CR7","unstructured":"Schneider, F.B. (ed.): Trust in Cyberspace, Committee on Information Systems Trustworthiness, National Research Council (1999)"},{"key":"4_CR8","unstructured":"Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Distributed System Security Symposium, San Diego, CA (February 2000)"},{"key":"4_CR9","unstructured":"Gates, W.H.: internal communication. Microsoft Corporation (2002)"},{"key":"4_CR10","unstructured":"Planning Report 02-3. The Economic Impacts of Inadequate Infrastructure for Software Testing, prepared by RTI for NIST, US Department of Commerce (May 2002)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the 24th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 1997) (January 1997)","DOI":"10.1145\/263699.263712"},{"key":"4_CR12","unstructured":"Turing, A.M.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating machines, Cambridge University Math. Lab., pp. 67\u201369 (1949)"},{"key":"4_CR13","volume-title":"Proc. IFIP Cong. 1962","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, J.: Towards a mathematical theory of computation. In: Proc. IFIP Cong. 1962. North-Holland, Amsterdam (1963)"},{"key":"4_CR14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Amer. Soc. Symp. Appl. Math.\u00a019, 19\u201331 (1967)","journal-title":"Proc. Amer. Soc. Symp. Appl. Math."},{"key":"4_CR15","unstructured":"King, J.C.: A Program Verifier, PhD thesis, Carnegie-Mellon University (1969)"},{"key":"4_CR16","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1985","unstructured":"Stroustrup, B.: The C++ Programming Language. Addison-Wesley, Reading (1985)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. In: OOPSLA 1999, pp. 132\u2013146 (1999)","DOI":"10.1145\/320385.320395"},{"key":"4_CR18","unstructured":"Haskell 98 language and libraries: the Revised Report, Journal of Functional Programming 13(1) (January 2003)"},{"key":"4_CR19","unstructured":"Hoare, C.A.R.: Assertions, Marktoberdorf Summer School (2002) (to appear)"},{"key":"4_CR20","volume-title":"An Electronic Purse: Specification, Refinement, and Proof, PRG-126","author":"S. Stepney","year":"2000","unstructured":"Stepney, S., Cooper, D., Woodcock, J.C.P.W.: An Electronic Purse: Specification, Refinement, and Proof, PRG-126. Oxford University Computing Laboratory, Oxford (2000)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Galloway, A.J., Cockram, T.J., McDermid, J.A.: Experiences with the application of discrete formal methods to the development of engine control software, Hise York (1998)","DOI":"10.1016\/S1474-6670(17)36335-8"},{"key":"4_CR22","doi-asserted-by":"crossref","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W.R. Bush","year":"2000","unstructured":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software \u2013 Practice and Experience\u00a0(30), 775\u2013802 (2000)","journal-title":"Software \u2013 Practice and Experience"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Evans, D., Larochelle, D.: Improving Security Using Extensible Lightweight Static Analysis. IEEE Software (January\/February 2002)","DOI":"10.1109\/52.976940"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A System and Language for Building System- Specific Static Analyses. In: PLDI 2000 (2002)","DOI":"10.21236\/ADA419593"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrotting of legacy code. In: 29th ACM Symposium on Principles of Programming Languages, Portland, OR (January 2002)","DOI":"10.1145\/503272.503286"},{"key":"4_CR26","unstructured":"Shankar, U., Talwar, K., Foster, J.S., Wagner, D.: Detecting format string vulnerabilities with type qualifiers. In: Proceedings of the 10th USENIX Security Symposium (2001)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Evans, D.: Static detection of dynamic memory errors. In: SIGPLAN Conference on Programming Languages Design and Implementation (1996)","DOI":"10.1145\/231379.231389"},{"key":"4_CR28","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Ruf, E.: Context-sensitive alias analysis reconsidered. Sigplan Notices\u00a030(6) (June 1995)","DOI":"10.1145\/223428.207112"},{"key":"4_CR30","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"4_CR31","first-page":"353","volume-title":"Model-Checking CSP, A Classical Mind: Essays in Honour of C.A.R. Hoare","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model-Checking CSP, A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353\u2013378. Prentice-Hall International, Englewood Cliffs (1994)"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: OSDI 2002 (2002) (to appear)","DOI":"10.1145\/1060289.1060297"},{"key":"4_CR33","first-page":"499","volume-title":"NATO ASI","author":"N. Shankar","year":"1997","unstructured":"Shankar, N.: Machine-assisted verification using theorem-proving and model checking, Mathematical Methods of Program Development. In: NATO ASI, vol.\u00a0138, pp. 499\u2013528. Springer, Heidelberg (1997)"},{"key":"4_CR34","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"HOL: A proof generating system for Higher-Order Logic, VLSI Specification, Verification and Synthesis","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: HOL: A proof generating system for Higher-Order Logic, VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer, Dordrecht (1988)"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0031813","volume-title":"Formal Methods in Computer-Aided Design","author":"N. Shankar","year":"1996","unstructured":"Shankar, N.: PVS: Combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 257\u2013264. Springer, Heidelberg (1996)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference (DAC 2001), Las Vegas (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: Proceedings of the 2002 International Symposium on Software Testing and Analysis, pp. 232\u2013242 (2002)","DOI":"10.1145\/566172.566213"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for eSC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"4_CR40","unstructured":"Milner, R.: Communicating and Mobile Systems: the pi Calculus, CUP (1999)"},{"key":"4_CR41","volume-title":"Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"4_CR42","volume-title":"Parallel Program Design: a Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: a Foundation. Addison-Wesley, Reading (1988)"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48743-3_1","volume-title":"ECOOP \u201999 - Object-Oriented Programming","author":"C.A.R. Hoare","year":"1999","unstructured":"Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol.\u00a01628, pp. 1\u201317. Springer, Heidelberg (1999)"},{"key":"4_CR45","unstructured":"Stepanov, A.: Meng Lee, Standard Template Library, Hewlett Packard (1994)"},{"issue":"1","key":"4_CR46","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The Verifying Compiler: a Grand Challenge for Computer Research. JACM\u00a050(1), 63\u201369 (2003)","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Modular Programming Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45213-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T13:20:52Z","timestamp":1559568052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45213-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540407966","9783540452133"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45213-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}