{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:10:40Z","timestamp":1725563440559},"publisher-location":"London","reference-count":24,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9781848829114"},{"type":"electronic","value":"9781848829121"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-84882-912-1_5","type":"book-chapter","created":{"date-parts":[[2010,8,20]],"date-time":"2010-08-20T12:27:13Z","timestamp":1282307233000},"page":"101-121","source":"Crossref","is-referenced-by-count":16,"title":["Forward with Hoare"],"prefix":"10.1007","author":[{"given":"Mike","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H\u00e9l\u00e8ne","family":"Collavizza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,7,21]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"J. Mantovani","year":"2009","unstructured":"Mantovani, J., Armando, A., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. Int. J. Software Tools Technol. Transfer 11(1), 69\u201383 February. (2009).","journal-title":"Int. J. Software Tools Technol. Transfer"},{"issue":"4","key":"5_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey \u2013 part I. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981).","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR3","unstructured":"ClarkeE., L.F., Kroening,D., Lerda F.: A tool for checking ansi-c programs. In: TACAS 2004, vol. 2988 of LNCS, pp. 168\u2013176. Springer-verlag (2004)."},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"SA Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978).","journal-title":"SIAM J. Comput."},{"issue":"4","key":"5_CR5","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficently computing static single assignment form and control dependence graph. Trans. Program. Lang. Systems,13(4), 451\u2013490 (1991).","journal-title":"Trans. Program. Lang. Systems"},{"key":"5_CR6","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (October 1976)."},{"key":"5_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, New York, Inc., New York, NY, USA (1990)."},{"key":"5_CR8","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Procsedings of the. Sympos. Applied. Mathematics., Vol. XIX, pp. 19\u201332. Amer. Math. Soc., Providence, R.I., (1967)."},{"key":"5_CR9","unstructured":"Gannod, G.C., Cheng, B.H.C.: Strongest postcondition semantics as the formal basis for reverse engineering. In: WCRE \u201995: Proceedings of the Second Working Conference on Reverse Engineering, p. 188, IEEE Computer Society. Washington, DC, USA (1995)."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Gries, D.: The Science of Programming. Springer (1981).","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"5_CR11","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, Xa. (eds.), POPL, pp. 232\u2013244. ACM (2004)."},{"issue":"10","key":"5_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"1","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. the ACM 12(10), 576\u2013580 October (1969).","journal-title":"Commun. the ACM"},{"key":"5_CR13","first-page":"135","volume":"3","author":"CAR Hoare","year":"1974","unstructured":"Hoare, C.A.R., Lauer, P.E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Inf. 3, 135\u2013153 (1974).","journal-title":"Acta Inf."},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S Igarashi","year":"1975","unstructured":"Igarashi, S., London, R.L., Luckham, D.C.: Automatic program verificationI: A logical basis and its implementation. Acta Inf. 4, 145\u2013182 (1975).","journal-title":"Acta Inf."},{"key":"5_CR15","volume-title":"Automatic program verification i: a logical basis and its implementation","author":"S Igarashi","year":"1973","unstructured":"Igarashi, S., London, R.L., Luckham, D.C.: Automatic program verification i: a logical basis and its implementation. Technical report, Stanford University, Stanford, CA, USA (1973)."},{"issue":"2","key":"5_CR16","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MAHC.2003.1203057","volume":"25","author":"CB Jones","year":"2003","unstructured":"Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput. 25(2), 26\u201349, (2003).","journal-title":"IEEE Ann. Hist. Comput."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"King, J.C.: A program verifier. In: IFIP Congress (1), pp. 234\u2013249 (1971).","DOI":"10.1038\/234249a0"},{"issue":"7","key":"5_CR18","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (July 1976).","journal-title":"Commun. ACM"},{"key":"5_CR19","unstructured":"Cornelius King, J.: A program verifier. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1970)."},{"key":"5_CR20","unstructured":"Luckham, D.C.: A brief account: Implementation and applications of a pascal program verifier (position statement). In: ACM \u201978: Proceedings of the 1978 Annual conference, pp. 786\u2013792 ACM, New York, NY, USA (1978)."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of 15th Annual Conference of the European Association for Computer Science Logic, vol. 2142 of Lecture Notes in Computer Science, pp. 1\u201319. Springer (September 2001).","DOI":"10.1007\/3-540-44802-0_1"},{"key":"5_CR22","unstructured":"Pasareanu, Co.S., Visser, W.: Verification of java programs using symbolic execution and invariant generation. In: Graf, S. Mounier, L. (eds.), SPIN, vol. 2989 of Lecture Notes in Computer Science, pp. 164\u2013181. Springer (2004)."},{"key":"5_CR23","unstructured":"von Henke, F.W, Luckham, D.C.: A methodology for verifying programs. In: Proceedings of the International Conference on Reliable Software, pp. 156\u2013164 ACM, New York, NY, USA (1975)."},{"key":"5_CR24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: an Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: an Introduction. MIT, Cambridge, MA, USA (1993)."}],"container-title":["Reflections on the Work of C.A.R. Hoare"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-84882-912-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,10]],"date-time":"2020-06-10T15:12:03Z","timestamp":1591801923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-84882-912-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781848829114","9781848829121"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-1-84882-912-1_5","relation":{},"subject":[],"published":{"date-parts":[[2010]]}}}