{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:08:19Z","timestamp":1725505699529},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787990"},{"type":"electronic","value":"9783540788003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_32","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:26:19Z","timestamp":1207124779000},"page":"428-442","source":"Crossref","is-referenced-by-count":13,"title":["Accelerating Interpolation-Based Model-Checking"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Caniart","sequence":"first","affiliation":[]},{"given":"Emmanuel","family":"Fleury","sequence":"additional","affiliation":[]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Zeitoun","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat Acceleration in Symbolic Model-Checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 474\u2013488. Springer, Heidelberg (2005)"},{"key":"32_CR2","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1145\/1250734.1250769","volume-title":"Proc. of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI 2007)","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path Invariants. In: Proc. of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI 2007), pp. 300\u2013309. ACM Press, New York (2007)"},{"key":"32_CR3","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Facult\u00e9 des Sciences Appliqu\u00e9es de l\u2019Universit\u00e9 de Li\u00e8ge (1999)"},{"issue":"1-3","key":"32_CR4","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/S0304-3975(03)00314-1","volume":"309","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B.: On Iterating Linear Transformations Over Recognizable Sets of Integers. Theoret. Comput. Sci.\u00a0309(1-3), 413\u2013468 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model-Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 403\u2013418. Springer, Heidelberg (2000)"},{"issue":"5","key":"32_CR6","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: CounterExample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Schwoon, S., Kiefer, S.: Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"32_CR8","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)"},{"issue":"2","key":"32_CR9","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.H.: Semigroups, Presburger Formulas and Languages. Pacific Journal of Mathematics\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific Journal of Mathematics"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"32_CR11","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/1181775.1181790","volume-title":"Proc. of 14th Symp. on Foundations of Software Engineering (FSE 2006)","author":"B. Gulavani","year":"2006","unstructured":"Gulavani, B., Henzinger, T.A., Kannan, Y., Nori, A., Rajamani, S.K.: Synergy: A New Algorithm for Property Checking. In: FSE 2006, pp. 117\u2013127. ACM Press, New York (2006)"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumbar, R., Sutre, G.: Lazy Abstraction. In: Proc. of 29th Symp. on Principles of Programming Languages (POPL 2002), pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"32_CR13","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., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"32_CR15","doi-asserted-by":"publisher","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. Journal of Theoritical Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Journal of Theoritical Computer Science"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"32_CR17","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du 1er congr\u00e8s de Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101 (1929)"}],"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-540-78800-3_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:22:50Z","timestamp":1619522570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_32","relation":{},"subject":[]}}