{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T13:52:34Z","timestamp":1746193954580,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545799"},{"type":"electronic","value":"9783662545805"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54580-5_21","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T06:50:09Z","timestamp":1490856609000},"page":"350-354","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs"],"prefix":"10.1007","author":[{"given":"Jera","family":"Hensel","sequence":"first","affiliation":[]},{"given":"Frank","family":"Emrich","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Str\u00f6der","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"21_CR1","unstructured":"AProVE. http:\/\/aprove.informatik.rwth-aachen.de\/"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Schmidt-Schau\u00df, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 155\u2013170. Dagstuhl Publishing (2011). doi:10.4230\/LIPIcs.RTA.2011.155","DOI":"10.4230\/LIPIcs.RTA.2011.155"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31762-0_9","volume-title":"Formal Verification of Object-Oriented Software","author":"M Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123\u2013141. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31762-0_9"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_22"},{"key":"21_CR5","unstructured":"Clang. http:\/\/clang.llvm.org"},{"key":"21_CR6","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 de Moura","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"21_CR7","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver, 2006. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"21_CR8","unstructured":"Eclipse. http:\/\/www.eclipse.org\/"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24605-3_37"},{"issue":"1","key":"21_CR10","doi-asserted-by":"publisher","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., 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(1), 3\u201331 (2017)","journal-title":"J. Autom. Reason."},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-41591-8_16","volume-title":"Software Engineering and Formal Methods","author":"J Hensel","year":"2016","unstructured":"Hensel, J., Giesl, J., Frohn, F., Str\u00f6der, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 234\u2013252. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-41591-8_16"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis and transformation. In: CGO 2004, pp. 55\u201388. IEEE (2004). doi:10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"21_CR13","unstructured":"Mono. http:\/\/www.mono-project.com\/"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-662-46681-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Str\u00f6der","year":"2015","unstructured":"Str\u00f6der, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: termination and memory safety of C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 417\u2013419. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_32"},{"issue":"1","key":"21_CR15","doi-asserted-by":"publisher","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(1), 33\u201365 (2017)","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54580-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:52:48Z","timestamp":1618973568000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54580-5_21"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545799","9783662545805"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54580-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}