{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T17:43:35Z","timestamp":1779385415192,"version":"3.53.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535868","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"139-150","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Abstract satisfaction"],"prefix":"10.1145","author":[{"given":"Vijay","family":"D'Silva","sequence":"first","affiliation":[{"name":"University of California, Berkeley, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"LPAR","author":"Bj\u00f8rner N.","year":"2008","unstructured":"N. Bj\u00f8rner , B. Duterte , and L. de Moura . Accelerating lemma learning using joins -- DPLL(t) . In LPAR , 2008 . N. Bj\u00f8rner, B. Duterte, and L. de Moura. Accelerating lemma learning using joins -- DPLL(t). In LPAR, 2008."},{"key":"e_1_3_2_2_2_1","volume-title":"VMCAI","author":"Brain M.","year":"2012","unstructured":"M. Brain , V. D'Silva , L. Haller , A. Griggio , and D. Kroening . An abstract interpretation of DPLL(T) . In VMCAI , 2012 . M. Brain, V. D'Silva, L. Haller, A. Griggio, and D. Kroening. An abstract interpretation of DPLL(T). In VMCAI, 2012."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_22"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763544"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_2_6_1","first-page":"77","volume-title":"FORMATS","author":"Cotton S.","year":"2010","unstructured":"S. Cotton . Natural domain SMT : A preliminary assessment . In FORMATS , pages 77 -- 91 , 2010 . S. Cotton. Natural domain SMT: A preliminary assessment. In FORMATS, pages 77--91, 2010."},{"key":"e_1_3_2_2_7_1","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"Cousot P.","year":"1981","unstructured":"P. Cousot . Semantic foundations of program analysis . In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications , chapter 10, pages 303 -- 342 . Prentice-Hall, Inc. , 1981 . P. Cousot. Semantic foundations of program analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303--342. Prentice-Hall, Inc., 1981."},{"key":"e_1_3_2_2_8_1","volume-title":"Calculational System Design","author":"Cousot P.","year":"1999","unstructured":"P. Cousot . The calculational design of a generic abstract interpreter . In M. Broy and R. Steinbr\u00fcggen, editors, Calculational System Design . NATO ASI Series F. IOS Press , Amsterdam , 1999 . P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbr\u00fcggen, editors, Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999."},{"key":"e_1_3_2_2_9_1","volume-title":"Abstract interpretation. MIT course 16.399","author":"Cousot P.","year":"2005","unstructured":"P. Cousot . Abstract interpretation. MIT course 16.399 , 2005 . P. Cousot. Abstract interpretation. MIT course 16.399, 2005."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2395116.2395120"},{"key":"e_1_3_2_2_15_1","volume-title":"Introduction to lattices and order","author":"Davey B. A.","year":"1990","unstructured":"B. A. Davey and H. A. Priestley . Introduction to lattices and order . Cambridge University Press , Cambridge, UK , 1990 . B. A. Davey and H. A. Priestley. Introduction to lattices and order. Cambridge University Press, Cambridge, UK, 1990."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_22"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429087"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_5"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"e_1_3_2_2_22_1","volume-title":"Failed literals in the Davis-Putnam procedure for SAT. Technical report","author":"Freeman J.W.","year":"1993","unstructured":"J.W. Freeman . Failed literals in the Davis-Putnam procedure for SAT. Technical report , Rutgers University , 1993 . J.W. Freeman. Failed literals in the Davis-Putnam procedure for SAT. Technical report, Rutgers University, 1993."},{"key":"e_1_3_2_2_23_1","first-page":"175","volume-title":"CAV","author":"Ganzinger H.","year":"2004","unstructured":"H. Ganzinger , G. Hagen , R. Nieuwenhuis , A. Oliveras , and C. Tinelli . DPLL(T): Fast decision procedures . In CAV , pages 175 -- 188 , 2004 . H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In CAV, pages 175--188, 2004."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134026"},{"key":"e_1_3_2_2_26_1","first-page":"131","volume-title":"FMCAD","author":"Haller L.","year":"2012","unstructured":"L. Haller , A. Griggio , M. Brain , and D. Kroening . Deciding floatingpoint logic with systematic abstraction . In FMCAD , pages 131 -- 140 , 2012 . L. Haller, A. Griggio, M. Brain, and D. Kroening. Deciding floatingpoint logic with systematic abstraction. In FMCAD, pages 131--140, 2012."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706309"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026228213080"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2023474.2023497"},{"key":"e_1_3_2_2_30_1","first-page":"308","volume-title":"CAV","author":"Kroening D.","year":"2004","unstructured":"D. Kroening , J. Ouaknine , S. A. Seshia , and O. Strichman . Abstraction-based satisfiability solving of Presburger arithmetic . In CAV , pages 308 -- 320 , July 2004 . D. Kroening, J. Ouaknine, S. A. Seshia, and O. Strichman. Abstraction-based satisfiability solving of Presburger arithmetic. In CAV, pages 308--320, July 2004."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1965974.1965991"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"e_1_3_2_2_33_1","first-page":"70","volume-title":"Workshop on Invariant Generation","author":"Leino K. R. M.","year":"2007","unstructured":"K. R. M. Leino and F. Logozzo . Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain . In Workshop on Invariant Generation , pages 70 -- 84 . RISC Report 07-07 , 2007 . K. R. M. Leino and F. Logozzo. Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain. In Workshop on Invariant Generation, pages 70--84. RISC Report 07-07, 2007."},{"key":"e_1_3_2_2_34_1","first-page":"1","volume-title":"CAV","author":"McMillan K. L.","year":"2003","unstructured":"K. L. McMillan . Interpolation and SAT-based model checking . In CAV , pages 1 -- 13 , 2003 . K. L. McMillan. Interpolation and SAT-based model checking. In CAV, pages 1--13, 2003."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_35"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_32"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041579"},{"issue":"3","key":"e_1_3_2_2_38_1","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BF00370684","article-title":"Algebraization of quantifier logics, an introductory overview","volume":"50","author":"N\u00e9meti I.","year":"1991","unstructured":"I. N\u00e9meti . Algebraization of quantifier logics, an introductory overview . Studia Logica: An International Journal for Symbolic Logic , 50 ( 3\/4 ): 485 -- 569 , 1991 . I. N\u00e9meti. Algebraization of quantifier logics, an introductory overview. Studia Logica: An International Journal for Symbolic Logic, 50(3\/4):485--569, 1991.","journal-title":"Studia Logica: An International Journal for Symbolic Logic"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_2_40_1","first-page":"39","volume-title":"Handbook of Logic in Computer Science","author":"Pitts A. M.","year":"2000","unstructured":"A. M. Pitts . Categorical logic . In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science , Volume 5 . Algebraic and Logical Structures, chapter 2, pages 39 -- 128 . Oxford University Press , 2000 . A. M. Pitts. Categorical logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, chapter 2, pages 39--128. Oxford University Press, 2000."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_2_42_1","volume-title":"Technical report","author":"Smith P.","year":"2010","unstructured":"P. Smith . The Galois connection of syntax and semantics. Technical report , Cambridge University , 2010 . P. Smith. The Galois connection of syntax and semantics. Technical report, Cambridge University, 2010."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_3"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_23"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_11"},{"key":"e_1_3_2_2_47_1","series-title":"CEUR Workshop Proceedings","volume-title":"IJCAR Doctoral Programme","author":"Tveretina O.","year":"2004","unstructured":"O. Tveretina . DPLL-based procedure for equality logic with uninterpreted functions. In IJCAR Doctoral Programme , volume 106 of CEUR Workshop Proceedings . CEUR-WS. org, 2004 . O. Tveretina. DPLL-based procedure for equality logic with uninterpreted functions. In IJCAR Doctoral Programme, volume 106 of CEUR Workshop Proceedings. CEUR-WS.org, 2004."}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535868","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535868","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535868"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":47,"alternative-id":["10.1145\/2535838.2535868","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535868","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535868","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}