{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:01Z","timestamp":1725568141924},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208136"},{"type":"electronic","value":"9783540398660"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-39866-0_1","type":"book-chapter","created":{"date-parts":[[2010,10,25]],"date-time":"2010-10-25T12:30:09Z","timestamp":1288009809000},"page":"1-12","source":"Crossref","is-referenced-by-count":3,"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":"1_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":"1_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. Compiler. In: Koskimies, K. (ed.) CC 1998. LNCS, vol.\u00a01383, pp. 302\u2013305. Springer, Heidelberg (1998)"},{"key":"1_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":"1_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":"1_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":"1_CR6","unstructured":"A congressional statement presented by the director of the National Infrastructure Protection Center See, http:\/\/www.fbi.gov\/congress\/congress02\/nipc072402.htm"},{"key":"1_CR7","unstructured":"Schneider, F.B. (ed.): Trust in Cyberspace, Committee on Information Systems Trustworthiness, National Research Council (1999)"},{"key":"1_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":"1_CR9","unstructured":"Gates, W.H.: Internal communication, Microsoft Corporation (2002)"},{"key":"1_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":"1_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997) (January 1997)","DOI":"10.1145\/263699.263712"},{"key":"1_CR12","unstructured":"Turing, A.M.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating machines, pp. 67\u201369. Cambridge University Math. Lab. (1949)"},{"key":"1_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":"1_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":"1_CR15","unstructured":"King, J.C.: A Program Verifier, PhD thesis, Carnegie-Mellon University (1969)"},{"key":"1_CR16","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1985","unstructured":"Stroustrup, B.: The C++ Programming Language. Adison-Wesley, Reading (1985)"},{"key":"1_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":"1_CR18","unstructured":"Haskell 98 language and libraries: the Revised Report. Journal of Functional Programming 13(1) (January 2003)"},{"key":"1_CR19","unstructured":"Hoare, C.A.R.: Assertions, Marktoberdorf Summer School (2002) (to appear)"},{"key":"1_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 (July 2000)"},{"key":"1_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":"1_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":"1_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":"1_CR24","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A System and Language for Building System-Specific Static Analyses. PLDI (2002)","DOI":"10.21236\/ADA419593"},{"key":"1_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":"1_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":"1_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":"1_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":"1_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":"1_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":"1_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":"1_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":"1_CR33","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/978-3-642-60858-2_26","volume-title":"Mathematical Methods of Program Development, NATO ASI","author":"N. Shankar","year":"1997","unstructured":"Shankar, N.: Machine-assisted verification using theorem-proving and model checking. In: Mathematical Methods of Program Development, NATO ASI, vol.\u00a0138, pp. 499\u2013528. Springer, Heidelberg (1997)"},{"key":"1_CR34","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"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. In: VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer, Dordrecht (1988)"},{"key":"1_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":"1_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 (DAC2001), Las Vegas (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"1_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":"1_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":"1_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":"1_CR40","unstructured":"Milner, R.: Communicating and Mobile Systems: the pi Calculus, CUP (1999)"},{"key":"1_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":"1_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":"1_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. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., 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":"1_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":"1_CR45","unstructured":"Stepanov, A., Lee, M.: Standard Template Library. Hewlett Packard (1994)"},{"issue":"50","key":"1_CR46","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"1","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The Verifying Compiler: a Grand Challenge for Computer Research. JACM\u00a01(50), 63\u201369 (2003)","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39866-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T17:23:15Z","timestamp":1559755395000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39866-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208136","9783540398660"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39866-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}