{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:47Z","timestamp":1725516527461},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_45","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"422-427","source":"Crossref","is-referenced-by-count":0,"title":["Tool Integration for Reasoned Programming"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Ireland","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"45_CR2","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)"},{"key":"45_CR3","volume-title":"International Conference on Dependable Systems and Networks (DSN 2002)","author":"P. Baudin","year":"2002","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 (DSN 2002), IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"45_CR4","unstructured":"Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Hayes, J.E., Richards, J., Michie, D. (eds.) Machine Intelligence, vol. 11, pp. 83\u2013124 (1988)"},{"key":"45_CR5","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","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. Springer, Heidelberg (1988); Longer version available from Edinburgh as DAI Research Paper No. 349"},{"key":"45_CR6","series-title":"Also available from Edinburgh as DAI Research Paper No. 513","first-page":"149","volume-title":"Essays in Honor of Woody Bledsoe","author":"A. Bundy","year":"1991","unstructured":"Bundy, A.: The use of proof plans for normalization. In: Boyer, R.S. (ed.) Essays in Honor of Woody Bledsoe, pp. 149\u2013166. Kluwer, Dordrecht (1991); Also available from Edinburgh as DAI Research Paper No. 513"},{"key":"45_CR7","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"45_CR8","unstructured":"de Moura, L., Owre, S., Rueb, H., Rushby, J., Shankar, N.: Integrating verification components: The interface is the message (2005), http:\/\/www.csl.sri.com\/users\/shankar\/shankar-drafts.html"},{"key":"45_CR9","first-page":"343","volume-title":"Proceedings of the 18th IEEE International Conference on Automated Software Engineering","author":"B.J. Ellis","year":"2003","unstructured":"Ellis, B.J., 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, Los Alamitos (2003); Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0010"},{"key":"45_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-24756-2_5","volume-title":"Integrated Formal Methods","author":"B.J. Ellis","year":"2004","unstructured":"Ellis, B.J., Ireland, A.: An integration of program analysis and automated theorem proving. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 67\u201386. Springer, Heidelberg (2004); Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0014"},{"key":"45_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Rustan, K., Leino, M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, Springer, Heidelberg (2001)"},{"key":"45_CR12","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":"45_CR13","volume-title":"VLSI Specification, Verification and Synthesis","author":"M.J. Gordon","year":"1988","unstructured":"Gordon, M.J.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, Kluwer, Dordrecht (1988)"},{"key":"45_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Hall, A., Chapman, R.: Correctness by construction: Developing a commercial secure system. IEEE Software\u00a019(2) (2002)","DOI":"10.1109\/52.976937"},{"key":"45_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","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, pp. 178\u2013189. Springer, Heidelberg (1992); Also available from Edinburgh as DAI Research Paper 592"},{"key":"45_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-61511-3_68","volume-title":"Automated Deduction - Cade-13","author":"A. Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Extensions to a Generalization Critic for Inductive Proof. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 47\u201361. Springer, Heidelberg (1996); Also available from Edinburgh as DAI Research Paper 786"},{"issue":"1\u20132","key":"45_CR18","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a016(1\u20132), 79\u2013111 (1996); Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"45_CR19","doi-asserted-by":"publisher","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. Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming\u00a09(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":"Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming"},{"issue":"4","key":"45_CR20","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s10817-006-9034-1","volume":"36","author":"A. Ireland","year":"2006","unstructured":"Ireland, A., Ellis, B.J., Cook, A., Chapman, R., Barnes, J.: An integrated approach to high integrity software verification. Journal of Automated Reasoning: Special Issue on Empirically Successful Automated Reasoning\u00a036(4), 379\u2013410 (2006)","journal-title":"Journal of Automated Reasoning: Special Issue on Empirically Successful Automated Reasoning"},{"issue":"1-4","key":"45_CR21","first-page":"65","volume":"29","author":"A. Ireland","year":"2001","unstructured":"Ireland, A., Stark, J.: Proof planning for strategy development. Annals of Mathematics and Artificial Intelligence\u00a029(1-4), 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":"Annals of Mathematics and Artificial Intelligence"},{"key":"45_CR22","doi-asserted-by":"crossref","unstructured":"King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost effective than testing? IEEE Trans. on SE\u00a026(8) (2000)","DOI":"10.1109\/32.879807"},{"key":"45_CR23","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 (April, 1991)"},{"key":"45_CR24","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 (April, 1991)"},{"key":"45_CR25","volume-title":"International Conference on Dependable Systems and Networks (DSN03)","author":"T. Nguyen","year":"2003","unstructured":"Nguyen, T., Ourghanlian, A.: Dependability assessment of safety-critical system software by static analysis methods. In: International Conference on Dependable Systems and Networks (DSN 2003), IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"45_CR26","unstructured":"PolySpace-Technologies, http:\/\/www.polyspace.com\/"},{"key":"45_CR27","unstructured":"Slind, K., Boulton, R.: Iterative dialogues and automated proof. In: Proceedings of the Second International Workshop on Frontiers of Combining Systems (FroCoS 1998), Amsterdam, The Netherlands (October, 1998)"},{"key":"45_CR28","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-15","author":"K. Slind","year":"1998","unstructured":"Slind, K., Gordon, M., Boulton, R., Bundy, A.: System description: An interface between CLAM and HOL. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, Springer, Heidelberg (1998); Earlier version available from Edinburgh as DAI Research Paper 885"},{"key":"45_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (1999); An earlier version is available from the Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM\/98\/2"},{"key":"45_CR30","unstructured":"Steel, G.: The importance of non-theorems and counterexamples in program verification. In: Submitted to the IFIP Working Conference on Verified Software: Theories, Tools, Experiments (2005)"},{"issue":"2","key":"45_CR31","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/360827.360850","volume":"17","author":"B. Wegbreit","year":"1974","unstructured":"Wegbreit, B.: The synthesis of loop predicates. Comm. ACM\u00a017(2), 102\u2013122 (1974)","journal-title":"Comm. ACM"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_45","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T07:44:07Z","timestamp":1557733447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}