{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:47:13Z","timestamp":1757544433739,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,11,5]]},"DOI":"10.1145\/1181775.1181789","type":"proceedings-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T20:15:56Z","timestamp":1168978556000},"page":"105-116","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":59,"title":["Interpolation for data structures"],"prefix":"10.1145","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[{"name":"University of New Mexico"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"UC Los Angeles"}]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[{"name":"Universit\u00e4t des Saarlandes"}]}],"member":"320","published-online":{"date-parts":[[2006,11,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"North-Holland","author":"Ackermann W.","year":"1954","unstructured":"W. Ackermann . Solvable Cases of the Decision Problem . North-Holland , 1954 . W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, 1954."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_3_2_1_4_1","first-page":"53","volume-title":"ECOOP 01","author":"Clarke D.G.","unstructured":"D.G. Clarke , J. Noble , and J.M. Potter . Simple ownership types for object containment . In ECOOP 01 , pages 53 -- 76 . D.G. Clarke, J. Noble, and J.M. Potter. Simple ownership types for object containment. In ECOOP 01, pages 53--76."},{"key":"e_1_3_2_1_5_1","first-page":"154","volume-title":"CAV 00, LNCS","author":"Clarke E. M.","year":"1855","unstructured":"E. M. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Counterexample-guided abstraction refinement . In CAV 00, LNCS 1855 , pages 154 -- 169 . Springer , 2000. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00, LNCS 1855, pages 154--169. Springer, 2000."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/230183"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_11_1","first-page":"72","volume-title":"CAV 97, LNCS 1254","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi . Construction of abstract state graphs with PVS . In CAV 97, LNCS 1254 , pages 72 -- 83 . Springer , 1997 . S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In CAV 97, LNCS 1254, pages 72--83. Springer, 1997."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200051513"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_6"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(94)00218-A"},{"key":"e_1_3_2_1_20_1","volume-title":"A reduction approach to decision procedures","author":"Kapur Deepak","year":"2005","unstructured":"Deepak Kapur and Calogero G. Zarba . A reduction approach to decision procedures . 2005 . Deepak Kapur and Calogero G. Zarba. A reduction approach to decision procedures. 2005."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_16"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/800233.807045"},{"key":"e_1_3_2_1_24_1","first-page":"729","article-title":"Axiomatizable classes of locally free algebras of certain types","volume":"3","author":"Mal'cev A.","year":"1962","unstructured":"A. Mal'cev . Axiomatizable classes of locally free algebras of certain types . Sibirsk. Mat. Zh. , 3 : 729 -- 743 , 1962 . A. Mal'cev. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Zh., 3:729--743, 1962.","journal-title":"Sibirsk. Mat. Zh."},{"key":"e_1_3_2_1_25_1","first-page":"1","volume-title":"LNCS 2725","author":"McMillan K.L.","year":"2003","unstructured":"K.L. McMillan . Interpolation and SAT-based model checking In CAV 03 , LNCS 2725 , pages 1 -- 13 . Springer , 2003 . K.L. McMillan. Interpolation and SAT-based model checking In CAV 03, LNCS 2725, pages 1--13. Springer, 2003."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/322203.322204"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_3_2_1_31_1","volume-title":"Software pioneers: contributions to software engineering","author":"Parnas D.L.","year":"2002","unstructured":"D.L. Parnas . The secret history of information hiding. In Software pioneers: contributions to software engineering . Springer , 2002 . D.L. Parnas. The secret history of information hiding. In Software pioneers: contributions to software engineering. Springer, 2002."},{"key":"e_1_3_2_1_32_1","first-page":"92","volume-title":"Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves","author":"Presburger M.","year":"1929","unstructured":"M. Presburger . \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt . In Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves , pages 92 -- 101 , 1929 . M. Presburger. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt. In Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves, pages 92--101, 1929."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871852"},{"key":"e_1_3_2_1_35_1","first-page":"500","volume-title":"CAV 02, LNCS 2404","author":"Stump A.","year":"2002","unstructured":"A. Stump , C.W. Barrett , and D.L. Dill . Cvc: A cooperating validity checker . In CAV 02, LNCS 2404 , pages 500 -- 504 . Springer , 2002 . A. Stump, C.W. Barrett, and D.L. Dill. Cvc: A cooperating validity checker. In CAV 02, LNCS 2404, pages 500--504. Springer, 2002."},{"key":"e_1_3_2_1_36_1","volume-title":"Proof Theory. North-Holland","author":"Takeuti G.","year":"1987","unstructured":"G. Takeuti . Proof Theory. North-Holland , 1987 . G. Takeuti. Proof Theory. North-Holland, 1987."},{"key":"e_1_3_2_1_37_1","volume-title":"University of California Press","author":"Tarski A.","year":"1951","unstructured":"A. Tarski . A Decision Method for Elementary Algebra and Geometry . University of California Press , 1951 . A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1951."},{"key":"e_1_3_2_1_38_1","first-page":"230","article-title":"On computable numbers, with an application to the Entscheidungsproblem","volume":"42","author":"Turing A. M.","year":"1936","unstructured":"A. M. Turing . On computable numbers, with an application to the Entscheidungsproblem . Proc. London Math. Society , 42 : 230 -- 265 , 1936 . A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Society, 42:230--265, 1936.","journal-title":"Proc. London Math. Society"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80003-8"},{"key":"e_1_3_2_1_40_1","first-page":"363","volume-title":"CADE 02, LNCS 2392","author":"Zarba C.G.","year":"2002","unstructured":"C.G. Zarba . Combining multisets with integers. In CADE 02, LNCS 2392 , pages 363 -- 376 . Springer , 2002 . C.G. Zarba. Combining multisets with integers. In CADE 02, LNCS 2392, pages 363--376. Springer, 2002."},{"key":"e_1_3_2_1_41_1","volume-title":"International Workshop on Unification","author":"Zarba C.G.","year":"2004","unstructured":"C.G. Zarba . A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator . In International Workshop on Unification , 2004 . C.G. Zarba. A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In International Workshop on Unification, 2004."}],"event":{"name":"SIGSOFT06\/FSE-14: SIGSOFT 2006 -14th International Symposium on the Foundations of Software Engineering","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Portland Oregon USA","acronym":"SIGSOFT06\/FSE-14"},"container-title":["Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1181775.1181789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T15:44:39Z","timestamp":1673365479000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1181775.1181789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11,5]]},"references-count":38,"alternative-id":["10.1145\/1181775.1181789","10.1145\/1181775"],"URL":"https:\/\/doi.org\/10.1145\/1181775.1181789","relation":{},"subject":[],"published":{"date-parts":[[2006,11,5]]},"assertion":[{"value":"2006-11-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}