{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T19:15:36Z","timestamp":1791141336576,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642333859","type":"print"},{"value":"9783642333866","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33386-6_16","type":"book-chapter","created":{"date-parts":[[2012,9,28]],"date-time":"2012-09-28T06:58:20Z","timestamp":1348815500000},"page":"187-202","source":"Crossref","is-referenced-by-count":33,"title":["Accelerating Interpolants"],"prefix":"10.1007","author":[{"given":"Hossein","family":"Hojjat","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Filip","family":"Kone\u010dn\u00fd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"16_CR1","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"Elvira Albert","year":"2010","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46(2) (February 2011)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative Completeness of Abstraction Refinement for Software Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 158\u2013172. Springer, Heidelberg (2002)"},{"issue":"1","key":"16_CR3","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des.\u00a015(1), 75\u201392 (1999)","journal-title":"Form. Methods Syst. Des."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332 (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300\u2013309 (2007)","DOI":"10.1145\/1273442.1250769"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-17511-4_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Blanc","year":"2010","unstructured":"Blanc, R., Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L.: ABC: Algebraic Bound Computation for Loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol.\u00a06355, pp. 103\u2013118. Springer, Heidelberg (2010)"},{"key":"16_CR7","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces, PhD Thesis, vol. 189. Collection des Publications de l\u2019Universit\u00e9 de Li\u00e8ge (1999)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists Are Counter Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-02658-4_15","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, F., Vojnar, T.: Automatic Verification of Integer Array Programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast Acceleration of Ultimately Periodic Relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-78800-3_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Caniart","year":"2008","unstructured":"Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating Interpolation-Based Model-Checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 428\u2013442. Springer, Heidelberg (2008)"},{"issue":"3","key":"16_CR13","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"16_CR15","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. CoRR, abs\/1011.0551 (2010)"},{"issue":"2","key":"16_CR16","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"Ginsburg, S., Spanier, E.: Bounded algol-like languages. Trans. of the AMS\u00a0113(2), 333\u2013368 (1964)","journal-title":"Trans. of the AMS"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M. Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of Trace Abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 69\u201385. Springer, Heidelberg (2009)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems (tool paper). In: FM (2012)","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/978-3-642-16242-8_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Leroux, J., R\u00fcmmer, P.: Interpolating Quantifier-Free Presburger Arithmetic. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 489\u2013503. Springer, Heidelberg (2010)"},{"issue":"1","key":"16_CR23","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1) (2005)","journal-title":"Theoretical Computer Science"},{"key":"16_CR24","unstructured":"Monniaux, D.: Personal Communication"},{"key":"16_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-77966-7_8","volume-title":"Hardware and Software: Verification and Testing","author":"A. Smr\u010dka","year":"2008","unstructured":"Smr\u010dka, A., Vojnar, T.: Verifying Parametrised Hardware Designs Via Counter Automata. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 51\u201368. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33386-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,4]],"date-time":"2019-07-04T04:21:49Z","timestamp":1562214109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33386-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642333859","9783642333866"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}