{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:05:05Z","timestamp":1743149105795,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_43","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"455-457","source":"Crossref","is-referenced-by-count":14,"title":["Ultimate Automizer with Array Interpolation"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Heizmann","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Dietsch","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Leike","sequence":"additional","affiliation":[]},{"given":"Betim","family":"Musa","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"43_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J. Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"43_CR2","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 471\u2013482. ACM (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"43_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M. Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 36\u201352. Springer, Heidelberg (2013)"},{"key":"43_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","volume-title":"Computer Aided Verification","author":"M. Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 797\u2013813. Springer, Heidelberg (2014)"},{"key":"43_CR5","unstructured":"Leike, J., Heizmann, M.: Geometric series as nontermination arguments for linear lasso programs. In: WST, pp. 55\u201359 (2014)"},{"key":"43_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-642-54862-8_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Leike","year":"2014","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 172\u2013186. Springer, Heidelberg (2014)"},{"key":"43_CR7","unstructured":"Leino, K.R.M.: This is Boogie 2. Manuscript working draft. Microsoft Research, Redmond (June 2008), \n                      \n                        http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml178.pdf"},{"key":"43_CR8","unstructured":"Musa, B.: Trace abstraction with unsatisfiable cores. Bachelor\u2019s thesis, University of Freiburg, Germany (2013)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:24:03Z","timestamp":1559139843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_43"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}