{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:23:15Z","timestamp":1725560595029},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213772"},{"type":"electronic","value":"9783540247562"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24756-2_5","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:18:31Z","timestamp":1280261911000},"page":"67-86","source":"Crossref","is-referenced-by-count":5,"title":["An Integration of Program Analysis and Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"Bill J.","family":"Ellis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Ireland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"issue":"1-2","key":"5_CR2","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"David A. Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. Journal of Automated Reasoning\u00a016(1-2) (1996)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"5_CR3","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"Jean-Francois Bergeretti","year":"1985","unstructured":"Bergeretti, J., Carr\u00e9, B.A.: Information-flow and data-flow analysis of while-programs. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a07(1) (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR4","volume-title":"CADE-9","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: CADE-9, Springer, Heidelberg (1988)"},{"key":"5_CR5","unstructured":"Bundy, A., Smaill, A., Hesketh, J.: Turning eureka steps into calculations in automatic program synthesis. In: Proceedings of UK IT (1990)"},{"issue":"2","key":"5_CR6","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"Alan Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062 (1993)","journal-title":"Artificial Intelligence"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"Alan Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: 10th International Conference on Automated Deduction (1990)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of the International Conference on Reliable Software (1975)","DOI":"10.1145\/800027.808436"},{"key":"5_CR9","volume-title":"Proceedings of ACM SigAda","author":"R. Chapman","year":"2002","unstructured":"Chapman, R., Amey, P.: Industrial strength exception freedom. In: Proceedings of ACM SigAda, Addison-Wesley, Reading (2002)"},{"key":"5_CR10","volume-title":"POPL-4","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL-4, ACM, New York (1977)"},{"key":"5_CR11","volume-title":"POPL-5","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL-5, ACM, New York (1978)"},{"key":"5_CR12","volume-title":"DARPA Information Survivability Conference and Expo (DISCEX)","author":"C. Cowan","year":"2000","unstructured":"Cowan, C., Wagle, P., Pu, C., Beattie, S., Walpole, J.: Buffer overflows: Attacks and defenses for the vulnerability of the decade. In: DARPA Information Survivability Conference and Expo (DISCEX), IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"5_CR13","unstructured":"Elspas, D., Green, M.W., Levitt, K.N., Waldinger, R.J.: Research in interactive program-proving techniques. In: SRI (1972)"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"1298","DOI":"10.1007\/BFb0002886","volume-title":"Euro-Par'97 Parallel Processing","author":"Andreas Ermedahl","year":"1997","unstructured":"Ermedahl, A., Gustafsson, J.: Deriving annotations for tight calculation of execution time. In: European Conference on Parallel Processing (1997)"},{"key":"5_CR15","unstructured":"ESA. Ariane 5 - flight 501 failure. Board of inquiry report, European Space Agency (1996)"},{"key":"5_CR16","volume-title":"Proceedings of FME","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Rustan, K., Leino, M.: Houdini, an annotation assistant for ESC\/Java. In: Proceedings of FME, Springer, Heidelberg (2001)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: Proceedings of PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"5_CR18","volume-title":"POPL-5","author":"S.M. German","year":"1978","unstructured":"German, S.M.: Automating proof of the absence of common runtime errors. In: POPL-5, ACM Press, New York (1978)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013060","volume-title":"Logic Programming and Automated Reasoning","author":"A. Ireland","year":"1992","unstructured":"Ireland, A.: The use of planning critics in mechanizing inductive proofs. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, Springer, Heidelberg (1992)"},{"key":"5_CR20","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/3-540-61511-3_68","volume-title":"Automated Deduction \u2014 Cade-13","author":"Andrew Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Extensions to a generalization critic for inductive proof. In: 13th Conference on Automated Deduction (1996)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning\u00a016(1-2) (1996)","DOI":"10.1007\/BF00244460"},{"issue":"2","key":"5_CR22","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1017\/S0956796899003408","volume":"9","author":"ANDREW IRELAND","year":"1999","unstructured":"Ireland, A., Bundy, A.: Automatic verification of functions with accumulating parameters. Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming\u00a09(2) (1999)","journal-title":"Journal of Functional Programming"},{"key":"5_CR23","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-3-540-24694-7_20","volume-title":"MICAI 2004: Advances in Artificial Intelligence","author":"Andrew Ireland","year":"2004","unstructured":"Ireland, A., Ellis, B.J., Ingulfsen, T.: Invariant patterns for program reasoning. Technical Report HW-MACS-TR-0011, School of Mathematical and Computer Sciences, Heriot-Watt University. Also to appear in the Proceedings of the Mexican International Conference on Artificial Intelligence 2004 (MICAI 2004) (2004)"},{"key":"5_CR24","unstructured":"Ireland, A., Stark, J.: On the automatic discovery of loop invariants. In: Proceedings of the 4th NASA Langley Formal Methods Workshop \u2013 NASA Conference Publication, vol. 3356 (1997)"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Ireland, A., Stark, J.: Proof planning for strategy development. Annals of Mathematics and Artificial Intelligence\u00a029(1-4) (2001)","DOI":"10.1023\/A:1018969728171"},{"key":"5_CR26","unstructured":"ISO. Reference manual for the Ada programming language. ISO\/IEC 8652, International Standards Organization (1995)"},{"key":"5_CR27","volume-title":"IEEE Annals of the History of Computing","author":"C.B. Jones","year":"2003","unstructured":"Jones, C.B.: The early search for tractable ways of reasoning about programs. In: IEEE Annals of the History of Computing, IEEE Computer Society, Los Alamitos (2003)"},{"key":"5_CR28","unstructured":"Katz, S.M., Manna, Z.: A heuristic approach to program verification. In: Proceedings of IJCAI 1973. IJCAI (1973)"},{"issue":"4","key":"5_CR29","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"Shmuel Katz","year":"1976","unstructured":"Katz, S.M., Manna, Z.: Logical analysis of programs. Communications of the ACM\u00a019(4) (1976)","journal-title":"Communications of the ACM"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for logic program synthesis. In: Proceedings of the 10th International Conference on Logic Programming (1993)","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"5_CR31","unstructured":"MatLab, http:\/\/www.mathworks.com\/"},{"key":"5_CR32","unstructured":"PolySpace-Technologies, http:\/\/www.polyspace.com\/"},{"key":"5_CR33","unstructured":"PURRS: The parma university\u2019s recurrence relation solver, http:\/\/www.cs.unipr.it\/purrs\/"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48958-4_15","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Stark","year":"1999","unstructured":"Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol.\u00a01559, p. 271. Springer, Heidelberg (1999)"},{"key":"5_CR35","volume-title":"14th IEEE International Conference on Automated Software Engineering","author":"J. Stark","year":"1999","unstructured":"Stark, J., Ireland, A.: Towards automatic imperative program synthesis through proof planning. In: 14th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, Los Alamitos (1999)"},{"key":"5_CR36","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, University Mathematical Laboratory, Cambridge, UK (1949)"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45127-7_27","volume-title":"Rewriting Techniques and Applications","author":"E. Visser","year":"2001","unstructured":"Visser, E.: Stratego: A language for program transformation based on rewriting strategies. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, p. 357. Springer, Heidelberg (2001)"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Whiting, L., Hill, M.: Safety analysis of hawk in flight monitor. In: Workshop on Program Analysis For Software Tools and Engineering (1999)","DOI":"10.1145\/316158.316173"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24756-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:33:45Z","timestamp":1559316825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24756-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213772","9783540247562"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24756-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}