{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:26Z","timestamp":1725557846813},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213666"},{"type":"electronic","value":"9783540399933"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-39993-3_8","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T18:30:36Z","timestamp":1277231436000},"page":"124-136","source":"Crossref","is-referenced-by-count":2,"title":["Towards the Verifying Compiler"],"prefix":"10.1007","author":[{"given":"Tony","family":"Hoare","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","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 \u2014 Practice and Experience\u00a0(30), 775\u2013802 (2000)","journal-title":"Software \u2014 Practice and Experience"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-07162-8_678","volume-title":"Mathematical Foundations of Computer Science 1974","author":"O.-J. Dahl","year":"1975","unstructured":"Dahl, O.-J.: An approach to correctness proofs of semicoroutines. In: Blikle, A. (ed.) MFCS 1974. LNCS, vol.\u00a028, pp. 157\u2013174. Springer, Heidelberg (1975)"},{"key":"8_CR3","unstructured":"Dahl, O.-J.: Can program proving be made practical? In: Les fondements de la programmation, Institut de recherch dinformatique et dautomatique, pp. 57\u2013114 (in English: ISBN 2726101844)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","first-page":"274","volume-title":"Abstract Software Specifications","author":"O.-J. Dahl","year":"1980","unstructured":"Dahl, O.-J.: Time sequences as a tool for describing program behaviour. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol.\u00a086, pp. 274\u2013290. Springer, Heidelberg (1980)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"VDM \u201990. VDM and Z - Formal Methods in Software Development","author":"O.-J. Dahl","year":"1990","unstructured":"Dahl, O.-J.: Object-orientation and formal techniques. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol.\u00a0428, pp. 1\u201311. Springer, Heidelberg (1990)"},{"key":"8_CR6","unstructured":"Dahl, O.-J.: A note on monitor versions. In: Millennial Perspectives in Computer Science, Palgrave, pp. 91\u201398 (2000)"},{"key":"8_CR7","unstructured":"Dahl, O.-J.: Verifiable programming, 269 pages. Prentice Hall, Englewood Cliffs (1992)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/BFb0019999","volume-title":"VDM \u201991","author":"O.-J. Dahl","year":"1991","unstructured":"Dahl, O.-J., Owe, O.: Formal development with ABEL. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol.\u00a0552, pp. 320\u2013362. Springer, Heidelberg (1991)"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/BF01933419","volume":"8","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: A Constructive Approach to the problem of Program Correctness. BIT\u00a08, 174\u2013186 (1968)","journal-title":"BIT"},{"key":"8_CR10","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":"8_CR11","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Amer. Soc. Symp. Appl. Math., vol.\u00a019, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"8_CR12","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"8_CR13","unstructured":"Gates, W.H.: internal communication, Microsoft Corporation (2002)"},{"issue":"10","key":"8_CR14","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. Comm. ACM\u00a012(10), 576\u2013580, 583 (1969)","journal-title":"Comm. ACM"},{"issue":"1","key":"8_CR15","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"},{"key":"8_CR16","unstructured":"Johnson, S.C.: Lint, a C program Checker. In: UNIX Programmers Manual, vol.\u00a02A, pp. 292\u2013303"},{"key":"8_CR17","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioural interface specification language for Java, Technical Report 98-060, Iowa State University, Department of Computer Science (August 2001)"},{"key":"8_CR18","unstructured":"Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC\/Java users manual. Tech note 2002.002, Compaq SRC (October 2000)"},{"key":"8_CR19","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":"8_CR20","volume-title":"Object-Oriented Software Constrcution","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Constrcution, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"8_CR21","first-page":"67","volume-title":"Report on a Conference on High Speed Automatic Calculating machines","author":"A.M. Turing","year":"1949","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., Cambridge (1949)"}],"container-title":["Lecture Notes in Computer Science","From Object-Orientation to Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39993-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T09:34:32Z","timestamp":1559208872000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39993-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213666","9783540399933"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39993-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}