{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:25Z","timestamp":1725562585356},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540214595"},{"type":"electronic","value":"9783540246947"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24694-7_20","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T13:40:16Z","timestamp":1280756416000},"page":"190-201","source":"Crossref","is-referenced-by-count":5,"title":["Invariant Patterns for Program Reasoning"],"prefix":"10.1007","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":"Tommy","family":"Ingulfsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_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":"20_CR2","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a016(1-2), 147\u2013180 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, Springer, Heidelberg (1988)"},{"key":"20_CR4","volume-title":"Proceedings of UK IT 1990","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., Smaill, A., Hesketh, J.: Turning eureka steps into calculations in automatic program synthesis. In: Proceedings of UK IT 1990, IEEE, Los Alamitos (1990)"},{"key":"20_CR5","doi-asserted-by":"publisher","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\u00a062, 185\u2013253 (1993)","journal-title":"Artificial Intelligence"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"German, S.M.: Automating proof of the absence of common runtime errors. In: Proceedings of 5th ACM Conference on Principles of Programming Languages (1978)","DOI":"10.1145\/512760.512772"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"German, S.M., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. on Software Engineering SE-1(1) (1975)","DOI":"10.1109\/TSE.1975.6312821"},{"key":"20_CR8","unstructured":"Ingulfsen, T.: Automatic generation of algorithmic properties: AutoGAP. BSc undergraduate dissertation project, School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh (2003)"},{"key":"20_CR9","series-title":"LNAI","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 (LNAI), vol.\u00a0624, Springer, Heidelberg (1992)"},{"key":"20_CR10","series-title":"LNAI","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 (LNAI), vol.\u00a01104, Springer, Heidelberg (1996)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning 16(1-2) (1996)","DOI":"10.1007\/BF00244460"},{"issue":"2","key":"20_CR12","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. Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming\u00a09(2), 225\u2013245 (1999)","journal-title":"Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming"},{"key":"20_CR13","unstructured":"Ireland, A., Stark, J.: On the automatic discovery of loop invariants. In: Proceedings of LFM 1997, NASA Conference Publication 3356 (1997)"},{"issue":"1-4","key":"20_CR14","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)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"20_CR15","unstructured":"Katz, S.M., Manna, Z.: A heuristic approach to program verification. In: Proceedings of IJCAI 1973 (1973)"},{"issue":"4","key":"20_CR16","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S.M. Katz","year":"1976","unstructured":"Katz, S.M., Manna, Z.: Logical analysis of programs. Communications of the ACM\u00a019(4), 188\u2013206 (1976)","journal-title":"Communications of the ACM"},{"key":"20_CR17","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":"20_CR18","unstructured":"Wegbreit, B.: Heuristic methods for mechanically deriving inductive assertions. In: Proceedings of IJCAI 1973 (1973)"},{"issue":"2","key":"20_CR19","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","MICAI 2004: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24694-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T14:53:11Z","timestamp":1548427991000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24694-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540214595","9783540246947"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24694-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}