{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T02:10:17Z","timestamp":1736561417751,"version":"3.32.0"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T00:00:00Z","timestamp":1159488000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,2]]},"DOI":"10.1007\/s10817-006-9034-1","type":"journal-article","created":{"date-parts":[[2006,9,28]],"date-time":"2006-09-28T09:51:06Z","timestamp":1159437066000},"page":"379-410","source":"Crossref","is-referenced-by-count":5,"title":["An Integrated Approach to High Integrity Software Verification"],"prefix":"10.1007","volume":"36","author":[{"given":"Andrew","family":"Ireland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bill J.","family":"Ellis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roderick","family":"Chapman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Janet","family":"Barnes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,9,29]]},"reference":[{"key":"9034_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL'02: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u20133. Portland, Oregon (2002)","DOI":"10.1145\/503272.503274"},{"key":"9034_CR2","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston, Massachusetts (2003)"},{"issue":"1\u20132","key":"9034_CR3","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. J. Autom. Reason. 16(1\u20132), 147\u2013180 (1996)","journal-title":"J. Autom. Reason."},{"key":"9034_CR4","doi-asserted-by":"crossref","unstructured":"Baudin, P., Pacalet, A., Raguideau, J., Schoen, D., Williams, N.: CAVEAT: A tool for software validation. In: International Conference on Dependable Systems and Networks (DSN02). IEEE Computer Society (2002)","DOI":"10.1109\/DSN.2002.1028953"},{"issue":"1","key":"9034_CR5","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"J.-F. Bergeretti","year":"1985","unstructured":"Bergeretti, J.-F., Carr\u00e9, B.A.: Information-flow and data-flow analysis of while-programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 37\u201361 (1985)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"3","key":"9034_CR6","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1017\/S0956796802004562","volume":"13","author":"B. Fischer","year":"2003","unstructured":"Fischer, B., Schumann, J.: Autobayes: A system for generating data analysis programs from statistical models. J. Funct. Program. 13(3), 483\u2013508 (2003)","journal-title":"J. Funct. Program."},{"key":"9034_CR7","unstructured":"Boyer, R.S., Moore, JS.: A Computational Logic Handbook. Perspectives in Computing, Vol. 23. Academic, Boston, Massachusetts (1988)"},{"key":"9034_CR8","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111\u2013120 (1988). Longer version available from Edinburgh as DAI Research Paper No. 349","DOI":"10.1007\/BFb0012826"},{"key":"9034_CR9","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge, England (2005)","DOI":"10.1017\/CBO9780511543326"},{"key":"9034_CR10","unstructured":"Bundy, A., Smaill, A., Hesketh, J.: Turning Eureka steps into calculations in automatic program synthesis. In: Clarke, S.L. (ed.) Proc. UK IT 90, pp. 221\u2013226 (1990a). Also available from Edinburgh as DAI Research Paper 448"},{"key":"9034_CR11","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62, 185\u2013253 (1993). Also available from Edinburgh as DAI Research Paper No. 567","journal-title":"Artificial Intelligence"},{"key":"9034_CR12","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. J. Autom. Reason. 7, 303\u2013324 (1991). Earlier version available from Edinburgh as DAI Research Paper No 413","journal-title":"J. Autom. Reason."},{"key":"9034_CR13","doi-asserted-by":"crossref","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster\u2013Clam system. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, Vol. 449 of Lecture Notes in Artificial Intelligence, pp. 647\u2013648. Springer (1990). Also available from Edinburgh as DAI Research Paper 507","DOI":"10.1007\/3-540-52885-7_123"},{"key":"9034_CR14","doi-asserted-by":"crossref","unstructured":"Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of International Conference on Reliable Software. Los Angeles, California (1975)","DOI":"10.1145\/800027.808436"},{"key":"9034_CR15","unstructured":"Chapman, R., Amey, P.: Industrial Strength Exception Freedom. In: Proc. ACM SigAda (2002)"},{"key":"9034_CR16","doi-asserted-by":"crossref","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 (1977a)","DOI":"10.1145\/512950.512973"},{"key":"9034_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: Mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, pp. 1\u201312 (1977b)","DOI":"10.1145\/800228.806926"},{"key":"9034_CR18","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) (2000)"},{"key":"9034_CR19","doi-asserted-by":"crossref","unstructured":"Ellis, B., Ireland, A.: Automation for exception freedom proofs. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 343\u2013346. IEEE Computer Society (2003). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0010","DOI":"10.1109\/ASE.2003.1240334"},{"key":"9034_CR20","doi-asserted-by":"crossref","unstructured":"Ellis, B., Ireland, A.: An integration of program analysis and automated theorem proving. In: Boiten, E., Derrick, J., Smith, G. (eds.) Proceedings of the 4th International Conference on Integrated Formal Methods (IFM-04), Vol. 2999 of Lecture Notes in Computer Science, pp. 67\u201386 (2004). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0014","DOI":"10.1007\/978-3-540-24756-2_5"},{"key":"9034_CR21","volume-title":"Research in Interactive Program-Proving Techniques","author":"D. Elspas","year":"1972","unstructured":"Elspas, D., Green, M., Levitt, K., Waldinger, R.: Research in Interactive Program-Proving Techniques. In: SRI, Menlo Park, California (1972)"},{"key":"9034_CR22","unstructured":"ESA: Ariane 5 \u2013 Flight 501 Failure. Board of Inquiry Report, European Space Agency (1996)"},{"key":"9034_CR23","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., S. Owre, H. Rue\u00df, and N. Shankar: ICS: Integrated Canonizer and Solver. In: Proc. CAV 2001 (2001)","DOI":"10.1007\/3-540-44585-4_22"},{"key":"9034_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC\/Java. In: Proceedings FME 2001 (2001)","DOI":"10.1007\/3-540-45251-6_29"},{"key":"9034_CR25","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended Static Checking for Java. In: Proceedings PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"9034_CR26","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, pp. 19\u201332. American Mathematical Society, Providence, Rhode Island (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"9034_CR27","doi-asserted-by":"crossref","unstructured":"German, S.: Automating proof of the absence of common runtime errors. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Conference on Principles of Programming Languages (1978)","DOI":"10.1145\/512760.512772"},{"key":"9034_CR28","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"9034_CR29","doi-asserted-by":"crossref","unstructured":"Ireland, A.: The use of planning critics in mechanizing inductive proofs. In: Voronkov, A. (ed.) International Conference on Logic Programming and Automated Reasoning (LPAR'92), pp. 178\u2013189. St. Petersburg (1992). Also available from Edinburgh as DAI Research Paper 592","DOI":"10.1007\/BFb0013060"},{"issue":"1\u20132","key":"9034_CR30","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1\u20132), 79\u2013111 (1996). Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9034_CR31","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1017\/S0956796899003408","volume":"9","author":"A. Ireland","year":"1999","unstructured":"Ireland, A., Bundy, A.: Automatic verification of functions with accumulating parameters. J. Funct. Program.: Special Issue on Theorem Proving & Functional Programming 9(2), 225\u2013245 (1999). A longer version is available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM\/97\/11","journal-title":"J. Funct. Program.: Special Issue on Theorem Proving & Functional Programming"},{"key":"9034_CR32","unstructured":"Ireland, A., Ellis, B., Cook, A., Chapman, R., Barnes, J.: An Integrated Approach to High Integrity Software Development (2006). Available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0027"},{"key":"9034_CR33","doi-asserted-by":"crossref","unstructured":"Ireland, A., Ellis, B., Ingulfsen, T.: Invariant patterns for program reasoning. In: Monroy, R., Arroyo-Figueroa, G., Sucar, L., Sossa, H. (eds.) Proceedings of the 3rd Mexican International Conference on Artificial Intelligence (MICAI-04), Vol. 2972 of Lecture Notes in Artificial Intelligence, pp. 190\u2013201 (2004). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0011","DOI":"10.1007\/978-3-540-24694-7_20"},{"key":"9034_CR34","unstructured":"Ireland, A., Stark, J.: On the automatic discovery of loop invariants. In: Proceedings of the Fourth NASA Langley Formal Methods Workshop \u2013 NASA Conference Publication 3356 (1997). Also available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM\/97\/1"},{"issue":"1\u20134","key":"9034_CR35","first-page":"65","volume":"29","author":"A. Ireland","year":"2001","unstructured":"Ireland, A., Stark, J.: Proof planning for strategy development. Ann. Math. and Artif. Intell. 29(1\u20134), 65\u201397 (2001). An earlier version is available as Research Memo RM\/00\/3, Dept. of Computing and Electrical Engineering, Heriot-Watt University","journal-title":"Ann. Math. and Artif. Intell."},{"issue":"1","key":"9034_CR36","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s10515-006-5467-3","volume":"13","author":"A. Ireland","year":"2005","unstructured":"Ireland, A., Stark, J.: Combining proof plans with partial order planning for imperative program synthesis. J. Autom. Softw. Eng. 13(1), 65\u2013105 (2005). An earlier version is available from the School of Mathematical and Computer Sciences, Heriot-Watt University, Technical Report HW-MACS-TR-0026","journal-title":"J. Autom. Softw. Eng."},{"key":"9034_CR37","unstructured":"ISO: Reference Manual for the Ada Programming Language. ISO\/IEC 8652, International Standards Organization (1995)"},{"issue":"3","key":"9034_CR38","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1015707001763","volume":"28","author":"P. Jani\u010di\u0107","year":"2002","unstructured":"Jani\u010di\u0107, P., Bundy, A.: A general setting for flexibly combining and augmenting decision procedures. J. Autom. Reason. 28(3), 257\u2013305 (2002)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9034_CR39","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S. Katz","year":"1976","unstructured":"Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188\u2013206 (1976)","journal-title":"Commun. ACM"},{"key":"9034_CR40","doi-asserted-by":"crossref","unstructured":"King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost effective than testing? IEEE Trans. SE 26(8), 675\u2013686 (2000)","DOI":"10.1109\/32.879807"},{"key":"9034_CR41","unstructured":"Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for logic program synthesis. In: Warren, D.S. (ed.) Proceedings of the 10th International Conference on Logic Programming (1993). Also available as Max-Planck-Institut f\u00fcr Informatik Report MPI-I-93-214 and Edinburgh DAI Research Report 638"},{"key":"9034_CR42","unstructured":"MoD: Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment. Interim Defence Standard 00-56, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (1991a)"},{"key":"9034_CR43","unstructured":"MoD: The procurement of safety critical software in defence equipment (Part 1: Requirements, Part 2: Guidance). Interim Defence Standard 00-55, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (1991b)"},{"key":"9034_CR44","doi-asserted-by":"crossref","unstructured":"Monroy, R., Bundy, A., Ireland, A.: Proof plans for the correction of false conjectures. In: Pfenning, F. (ed.) 5th International Conference on Logic Programming and Automated Reasoning, LPAR'94, pp. 54\u201368. Kiev, Ukraine (1994). Also available from Edinburgh as DAI Research Paper 681","DOI":"10.1007\/3-540-58216-9_29"},{"key":"9034_CR45","unstructured":"(NCSP), N. C. S.P.: Improving Security across the Software Development Lifecycle. http:\/\/www.cyberpartnership.org (2004)"},{"key":"9034_CR46","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"9034_CR47","unstructured":"Polyspace, PolySpace-Technologies. http:\/\/www.polyspace.com\/"},{"key":"9034_CR48","unstructured":"PURRS, PURRS: The Parma University's Recurrence Relation Solver. http:\/\/www.cs.unipr.it\/purrs\/"},{"key":"9034_CR49","doi-asserted-by":"crossref","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic construction of hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27\u201329, 2003, Proceedings, Vol. 2895 of Lecture Notes in Computer Science, pp. 230\u2013245 (2003)","DOI":"10.1007\/978-3-540-40018-9_16"},{"key":"9034_CR50","doi-asserted-by":"crossref","unstructured":"Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) Logic-Based Program Synthesis and Transformation, Vol. 1559 of Lecture Notes in Computer Science, pp. 271-288. Springer (1998). An earlier version is available from the Dept. of Computing and Electrical Engineering, Heriot-Watt University, Berlin, Research Memo RM\/98\/2","DOI":"10.1007\/3-540-48958-4_15"},{"key":"9034_CR51","doi-asserted-by":"crossref","unstructured":"Visser, E.: Stratego: A Language for Program Transformation based on Rewriting Strategies. System Description of Stratego 0.5. In: Rewriting Techniques and Applications (RTA) (2001)","DOI":"10.1007\/3-540-45127-7_27"},{"key":"9034_CR52","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":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9034-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9034-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9034-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T01:30:53Z","timestamp":1736559053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9034-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9,29]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,1,2]]}},"alternative-id":["9034"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9034-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2006,9,29]]}}}