{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:04:58Z","timestamp":1765667098751},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319127354"},{"type":"electronic","value":"9783319127361"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_18","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"334-353","source":"Crossref","is-referenced-by-count":12,"title":["Automatic Constrained Rewriting Induction towards Verifying Procedural Programs"],"prefix":"10.1007","author":[{"given":"Cynthia","family":"Kop","sequence":"first","affiliation":[]},{"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. Journal of Symbolic Computation\u00a023(1), 47\u201377 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Voronkov, A., Robinson, A. (eds.) Handbook of Automated Reasoning, pp. 845\u2013911. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511543326"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 277\u2013293. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_22"},{"key":"18_CR5","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-31365-3_20","volume-title":"Automated Reasoning","author":"S. Falke","year":"2012","unstructured":"Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 241\u2013255. Springer, Heidelberg (2012)"},{"key":"18_CR6","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schau\u00df, M. (ed.) 22nd International Conference on Rewriting Techniques and Applications (RTA), Dagstuhl, Leibniz. LIPIcs, vol.\u00a010, pp. 41\u201350 (2011)"},{"key":"18_CR7","unstructured":"Falke, S.: Term Rewriting with Built-In Numbers and Collection Data Structures. Ph.D. thesis, University of New Mexico, Albuquerque, NM, USA (2009)"},{"key":"18_CR8","unstructured":"Furuichi, Y., Nishida, N., Sakai, M., Kusakari, K., Sakabe, T.: Approach to procedural-program verification based on implicit induction of constrained term rewriting systems. IPSJ Transactions on Programming\u00a01(2), 100\u2013121 (2008) (in Japanese)"},{"key":"18_CR9","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2000)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/10930755_9","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Kapur","year":"2003","unstructured":"Kapur, D., Sakhanenko, N.A.: Automatic generation of generalization lemmas for proving properties of tail-recursive definitions. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 136\u2013154. Springer, Heidelberg (2003)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/3-540-61511-3_112","volume-title":"Automated Deduction - Cade-13","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: Lemma discovery in automated induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 538\u2013552. Springer, Heidelberg (1996)"},{"key":"18_CR12","unstructured":"Kop, C.: Termination of LCTRSs. In: 13th International Workshop on Termination (WST), pp. 59\u201363 (2013)"},{"key":"18_CR13","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-40885-4_24","volume-title":"Frontiers of Combining Systems","author":"C. Kop","year":"2013","unstructured":"Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol.\u00a08152, pp. 343\u2013358. Springer, Heidelberg (2013)"},{"key":"18_CR14","unstructured":"Kop, C., Nishida, N.: Towards verifying procedural programs using constrained rewriting induction. Technical report, University of Innsbruck (2014), \n                    \n                      http:\/\/arxiv.org\/abs\/1409.0166"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR16","unstructured":"Nakabayashi, N., Nishida, N., Kusakari, K., Sakabe, T., Sakai, M.: Lemma generation method in rewriting induction for constrained term rewriting systems. Computer Software\u00a028(1), 173\u2013189 (2010) (in Japanese)"},{"key":"18_CR17","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java bytecode by term rewriting. In: Lynch, C. (ed.) 21st International Conference on Rewriting Techniques and Applications (RTA), Dagstuhl, Leibniz. LIPIcs, vol.\u00a06, pp. 259\u2013276 (2010)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-52885-7_86","volume-title":"10th International Conference on Automated Deduction","author":"U.S. Reddy","year":"1990","unstructured":"Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 162\u2013177. Springer, Heidelberg (1990)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-22531-4_9","volume-title":"Functional and Constraint Logic Programming","author":"T. Sakata","year":"2011","unstructured":"Sakata, T., Nishida, N., Sakabe, T.: On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs. In: Kuchen, H. (ed.) WFLP 2011. LNCS, vol.\u00a06816, pp. 138\u2013155. Springer, Heidelberg (2011)"},{"key":"18_CR20","unstructured":"Sakata, T., Nishida, N., Sakabe, T., Sakai, M., Kusakari, K.: Rewriting induction for constrained term rewriting systems. IPSJ Transactions on Programming\u00a02(2), 80\u201396 (2009) (in Japanese)"},{"issue":"1-3","key":"18_CR21","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.tcs.2004.05.022","volume":"323","author":"P. Urso","year":"2004","unstructured":"Urso, P., Kounalis, E.: Sound generalizations in mathematical induction. Theoretical Computer Science\u00a0323(1-3), 443\u2013471 (2004)","journal-title":"Theoretical Computer Science"},{"key":"18_CR22","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1613\/jair.275","volume":"4","author":"T. Walsh","year":"1996","unstructured":"Walsh, T.: A divergence critic for inductive proof. Journal of Artificial Intelligence Research\u00a04, 209\u2013235 (1996)","journal-title":"Journal of Artificial Intelligence Research"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12736-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T03:54:28Z","timestamp":1559015668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}