{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:40Z","timestamp":1725903400992},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_28","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"454-471","source":"Crossref","is-referenced-by-count":5,"title":["Certifying Safety and Termination Proofs for Integer Transition Systems"],"prefix":"10.1007","author":[{"given":"Marc","family":"Brockschmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastiaan J. C.","family":"Joosten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: FMOODS 2008, pp. 2\u201318","key":"28_CR1","DOI":"10.1007\/978-3-540-68863-1_2"},{"issue":"4","key":"28_CR2","doi-asserted-by":"crossref","first-page":"987","DOI":"10.1007\/s10270-015-0476-y","volume":"15","author":"E Albert","year":"2016","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: A formal verification framework for static analysis. Softw. Syst. Model. 15(4), 987\u20131012 (2016)","journal-title":"Softw. Syst. Model."},{"doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: FSE 2016, pp. 326\u2013337. ACM (2016)","key":"28_CR3","DOI":"10.1145\/2950290.2950351"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-40229-1_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 25\u201344. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_4"},{"issue":"4","key":"28_CR5","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: TACAS 2017 (to appear)","key":"28_CR6","DOI":"10.1007\/978-3-662-54577-5_6"},{"doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: ICALP 2005, pp. 1349\u20131361","key":"28_CR7","DOI":"10.1007\/11523468_109"},{"doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: CAV 2013, pp. 413\u2013429","key":"28_CR8","DOI":"10.1007\/978-3-642-39799-8_28"},{"doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: TACAS 2016, pp. 387\u2013393","key":"28_CR9","DOI":"10.1007\/978-3-662-49674-9_22"},{"doi-asserted-by":"crossref","unstructured":"Caleiro, C., Gon\u00e7alves, R.: On the algebraization of many-sorted logics. In: WADT 2006, pp. 21\u201336","key":"28_CR10","DOI":"10.1007\/978-3-540-71998-4_2"},{"unstructured":"Cho, S., Kang, J., Choi, J., Yi, K.: SparrowBerry: a verified validator for an industrial-strength static analyzer. http:\/\/ropas.snu.ac.kr\/sparrowberry\/","key":"28_CR11"},{"doi-asserted-by":"crossref","unstructured":"Contejean, E., Paskevich, A., Urbain, X., Courtieu, P., Pons, O., Forest, J.: A3PAT, an approach for certified automated termination proofs. In: PEPM 2010, pp. 63\u201372","key":"28_CR12","DOI":"10.1145\/1706356.1706370"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS 2013, pp. 47\u201361","key":"28_CR13","DOI":"10.1007\/978-3-642-36742-7_4"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415\u2013426","key":"28_CR14","DOI":"10.1145\/1133981.1134029"},{"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 1977, pp. 238\u2013252 (1977)","key":"28_CR15","DOI":"10.1145\/512950.512973"},{"unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA 2011, pp. 41\u201350","key":"28_CR16"},{"key":"28_CR17","first-page":"1","volume":"124","author":"J Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen Ungleichungen. J. f\u00fcr die reine Angew. Math. 124, 1\u201327 (1902)","journal-title":"J. f\u00fcr die reine Angew. Math."},{"key":"28_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58, 3\u201331 (2017)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Heule, M.J., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD 2013, pp. 181\u2013188. IEEE","key":"28_CR19","DOI":"10.1109\/FMCAD.2013.6679408"},{"doi-asserted-by":"crossref","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL 2015, pp. 247\u2013259","key":"28_CR20","DOI":"10.1145\/2676726.2676966"},{"issue":"4","key":"28_CR21","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine and compiler. ACM Trans. Progr. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: CAV 2014, pp. 17\u201334","key":"28_CR22","DOI":"10.1007\/978-3-319-08867-9_2"},{"doi-asserted-by":"crossref","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014, pp. 325\u2013340","key":"28_CR23","DOI":"10.1007\/978-3-319-08970-6_21"},{"issue":"7","key":"28_CR24","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"1","key":"28_CR25","doi-asserted-by":"crossref","first-page":"57","DOI":"10.15388\/Informatica.2010.273","volume":"21","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107, F., Jani\u010di\u0107, P.: Formal correctness proof for DPLL procedure. Informatica 21(1), 57\u201378 (2010)","journal-title":"Informatica"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K.: Lazy abstraction with interpolants. In: CAV 2006, pp. 123\u2013136","key":"28_CR26","DOI":"10.1007\/11817963_14"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"issue":"2","key":"28_CR28","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear quantifier elimination. J. Autom. Reason. 45(2), 189\u2013212 (2010)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: RTA 2010, pp. 259\u2013276","key":"28_CR29","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"28_CR30","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)"},{"doi-asserted-by":"crossref","unstructured":"Spasi\u0107, M., Mari\u0107, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012, pp. 434\u2013449","key":"28_CR31","DOI":"10.1007\/978-3-642-32759-9_35"},{"issue":"3","key":"28_CR32","doi-asserted-by":"crossref","first-page":"8: 1","DOI":"10.1145\/1709093.1709095","volume":"32","author":"F Spoto","year":"2010","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyser for Java Bytecode based on path-length. ACM Trans. Progr. Lang. Syst. 32(3), 8: 1\u20138: 70 (2010)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: UITP 2014, EPTCS, vol. 167, pp. 61\u201372 (2014)","key":"28_CR33","DOI":"10.4204\/EPTCS.167.8"},{"key":"28_CR34","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10817-016-9389-x","volume":"58","author":"T Str\u00f6der","year":"2017","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P., Aschermann, C.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58, 33\u201365 (2017)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs 2009, pp. 452\u2013468","key":"28_CR35","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"28_CR36","first-page":"234","volume":"8","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of proof in prepositional calculus. Stud. Constr. Math. Math. Logic Part II 8, 234\u2013259 (1968)","journal-title":"Stud. Constr. Math. Math. Logic Part II"},{"doi-asserted-by":"crossref","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: TACAS 2016, pp. 54\u201370","key":"28_CR37","DOI":"10.1007\/978-3-662-49674-9_4"},{"issue":"2","key":"28_CR38","doi-asserted-by":"crossref","first-page":"105","DOI":"10.2307\/2266241","volume":"17","author":"H Wang","year":"1952","unstructured":"Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105\u2013116 (1952)","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL 2012, pp. 427\u2013440","key":"28_CR39","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T22:39:29Z","timestamp":1602455969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}