{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:56Z","timestamp":1750306556209,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,13]],"date-time":"2015-01-13T00:00:00Z","timestamp":1421107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001825","name":"Danish Agency for Science, Technology and Innovation","doi-asserted-by":"publisher","award":["FNU 10-084290."],"award-info":[{"award-number":["FNU 10-084290."]}],"id":[{"id":"10.13039\/501100001825","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["318337"],"award-info":[{"award-number":["318337"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,13]]},"DOI":"10.1145\/2678015.2682544","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T13:51:05Z","timestamp":1418997065000},"page":"85-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Constraint Specialisation in Horn Clause Verification"],"prefix":"10.1145","author":[{"given":"Bishoksan","family":"Kafle","sequence":"first","affiliation":[{"name":"Roskilde University, Roskilde, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John P.","family":"Gallagher","sequence":"additional","affiliation":[{"name":"Roskilde University, Roskilde, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,1,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/6012.15399"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"F.\n      Benoy\n     and \n      A.\n      King\n  . \n  Inferring argument size relationships with CLP(R)\n  . In J. P. Gallagher editor Logic-Based Program Synthesis and Transformation (LOPSTR\n  '96) volume \n  1207\n   of \n  Springer-Verlag LNCS pages \n  204\n  --\n  223 August \n  1996\n  .   F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher editor Logic-Based Program Synthesis and Transformation (LOPSTR'96) volume 1207 of Springer-Verlag LNCS pages 204--223 August 1996.","DOI":"10.1007\/3-540-62718-9_12"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"N.\n      Bj\u00f8rner K. L.\n      McMillan and \n      A.\n      Rybalchenko\n  . \n  On solving universally quantified horn clauses\n  . In F. Logozzo and M. F\u00e4hndrich editors SAS volume \n  7935\n   of \n  LNCS pages \n  105\n  --\n  125\n  . \n  Springer 2013\n  .  N. Bj\u00f8rner K. L. McMillan and A. Rybalchenko. On solving universally quantified horn clauses. In F. Logozzo and M. F\u00e4hndrich editors SAS volume 7935 of LNCS pages 105--125. Springer 2013.","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00064-X"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426899"},{"key":"e_1_3_2_1_15_1","unstructured":"E.\n      De Angelis F.\n      Fioravanti A.\n      Pettorossi and \n      M.\n      Proietti\n  . \n  Verimap: A tool for verifying programs through transformations\n  . In E. Abraham and K. Havelund editors TACAS volume \n  8413\n   of \n  LNCS pages \n  568\n  --\n  574\n  . \n  Springer 2014\n  . ISBN 978--3--642--54861--1.  E. De Angelis F. Fioravanti A. Pettorossi and M. Proietti. Verimap: A tool for verifying programs through transformations. In E. Abraham and K. Havelund editors TACAS volume 8413 of LNCS pages 568--574. Springer 2014. ISBN 978--3--642--54861--1."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90050-7"},{"key":"e_1_3_2_1_17_1","volume-title":"ICOT","author":"Fujita H.","year":"1987","unstructured":"H. Fujita . An algorithm for partial evaluation with constraints. Technical Report TR-258 , ICOT , 1987 . H. Fujita. An algorithm for partial evaluation with constraints. Technical Report TR-258, ICOT, 1987."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154640"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of Meta90 Workshop on Meta Programming in Logic. Katholieke Universiteit Leuven","author":"Gallagher J. P.","year":"1990","unstructured":"J. P. Gallagher and M. Bruynooghe . Some low-level source transformations for logic programs . In Proceedings of Meta90 Workshop on Meta Programming in Logic. Katholieke Universiteit Leuven , Belgium , 1990 . J. P. Gallagher and M. Bruynooghe. Some low-level source transformations for logic programs. In Proceedings of Meta90 Workshop on Meta Programming in Logic. Katholieke Universiteit Leuven, Belgium, 1990."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-1-4471-3560-9_11","volume-title":"Logic Program Synthesis and Transformation,Workshops in Computing","author":"Gallagher J. P.","year":"1993","unstructured":"J. P. Gallagher and D. de Waal . Deletion of redundant unary type predicates from logic programs . In K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation,Workshops in Computing , pages 151 -- 167 . Springer-Verlag , 1993 . J. P. Gallagher and D. de Waal. Deletion of redundant unary type predicates from logic programs. In K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation,Workshops in Computing, pages 151--167. Springer-Verlag, 1993."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the International Conference on Logic Programming (ICLP'94)","author":"Gallagher J. P.","year":"1994","unstructured":"J. P. Gallagher and D. deWaal . Fast and precise regular approximation of logic programs. In P. Van Hentenryck, editor , Proceedings of the International Conference on Logic Programming (ICLP'94) , Santa Margherita Ligure, Italy. MIT Press , 1994 . J. P. Gallagher and D. deWaal. Fast and precise regular approximation of logic programs. In P. Van Hentenryck, editor, Proceedings of the International Conference on Logic Programming (ICLP'94), Santa Margherita Ligure, Italy. MIT Press, 1994."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037136"},{"key":"e_1_3_2_1_23_1","volume-title":"Failure tabled constraint logic programming by interpolation. TPLP, 13(4--5):593--607","author":"Gange G.","year":"2013","unstructured":"G. Gange , J. A. Navas , P. Schachte , H. S\u00f8ndergaard , and P. J. Stuckey . Failure tabled constraint logic programming by interpolation. TPLP, 13(4--5):593--607 , 2013 . G. Gange, J. A. Navas, P. Schachte, H. S\u00f8ndergaard, and P. J. Stuckey. Failure tabled constraint logic programming by interpolation. TPLP, 13(4--5):593--607, 2013."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_46"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_16"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58485-4_43"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_32"},{"key":"e_1_3_2_1_30_1","volume-title":"Partial Evaluation and Automatic Software Generation","author":"Jones N.","year":"1993","unstructured":"N. Jones , C. Gomard , and P. Sestoft . Partial Evaluation and Automatic Software Generation . Prentice Hall , 1993 . N. Jones, C. Gomard, and P. Sestoft. Partial Evaluation and Automatic Software Generation. Prentice Hall, 1993."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647166.760064"},{"key":"e_1_3_2_1_32_1","unstructured":"H. J.\n      Komorowski\n    .\n  An introduction to partial deduction\n  . In A. Pettorossi editor META volume \n  649\n   of \n  LNCS pages \n  49\n  --\n  69\n  . \n  Springer 1992\n  . ISBN 3--540--56282--6.   H. J. Komorowski. An introduction to partial deduction. In A. Pettorossi editor META volume 649 of LNCS pages 49--69. Springer 1992. ISBN 3--540--56282--6."},{"key":"e_1_3_2_1_33_1","volume-title":"Logic Program Synthesis and Transformation (LOPSTR'97)","author":"Lafave L.","year":"1998","unstructured":"L. Lafave and J. P. Gallagher . Partial evaluation of functional logic programs in rewriting-based languages . In N. Fuchs, editor, Logic Program Synthesis and Transformation (LOPSTR'97) , Springer-Verlag LNCS , 1998 . L. Lafave and J. P. Gallagher. Partial evaluation of functional logic programs in rewriting-based languages. In N. Fuchs, editor, Logic Program Synthesis and Transformation (LOPSTR'97), Springer-Verlag LNCS, 1998."},{"key":"e_1_3_2_1_34_1","series-title":"LNCS","first-page":"492","volume-title":"T. Bultan and P.-A","author":"Lakhdar-Chaouch L.","year":"2011","unstructured":"L. Lakhdar-Chaouch , B. Jeannet , and A. Girault . Widening with thresholds for programs with complex control graphs . In T. Bultan and P.-A . Hsiung, editors, ATVA 2011 , volume 6996 of LNCS , pages 492 -- 502 . Springer , 2011. L. Lakhdar-Chaouch, B. Jeannet, and A. Girault. Widening with thresholds for programs with complex control graphs. In T. Bultan and P.-A. Hsiung, editors, ATVA 2011, volume 6996 of LNCS, pages 492--502. Springer, 2011."},{"key":"e_1_3_2_1_35_1","series-title":"LNCS","first-page":"271","volume-title":"J. Hatcliff, T. \u00c6","author":"Leuschel M.","year":"1999","unstructured":"M. Leuschel . Advanced logic program specialisation . In J. Hatcliff, T. \u00c6 . Mogensen, and P. Thiemann, editors, Partial Evaluation - Practice and Theory, volume 1706 of LNCS , pages 271 -- 292 . Springer , 1999 . M. Leuschel. Advanced logic program specialisation. In J. Hatcliff, T. \u00c6. Mogensen, and P. Thiemann, editors, Partial Evaluation - Practice and Theory, volume 1706 of LNCS, pages 271--292. Springer, 1999."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/982158.982159"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"M.\n      Leuschel\n     and \n      T.\n      Massart\n  . \n  Infinite state model checking by abstract interpretation and program specialisation\n  . In A. Bossi editor LOPSTR'99 volume \n  1817\n   of \n  LNCS pages \n  62\n  --\n  81\n  . \n  Springer 1999\n  .   M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi editor LOPSTR'99 volume 1817 of LNCS pages 62--81. Springer 1999.","DOI":"10.1007\/10720327_5"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054108006066"},{"key":"e_1_3_2_1_39_1","volume-title":"Proc. Fifth International Conference on Logic programming","author":"Marriott K.","year":"1988","unstructured":"K. Marriott , L. Naish , and J.-L. Lassez . Most specific logic programs . In Proc. Fifth International Conference on Logic programming , Seattle, WA. MIT Press , 1988 . K. Marriott, L. Naish, and J.-L. Lassez. Most specific logic programs. In Proc. Fifth International Conference on Logic programming, Seattle, WA. MIT Press, 1988."},{"key":"e_1_3_2_1_40_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/978-3-642-23702-7_27","volume-title":"Static Analysis - 18th International Symposium, SAS","author":"Monniaux D.","year":"2011","unstructured":"D. Monniaux and L. Gonnord . Using bounded model checking to focus fixpoint iterations . In E. Yahav, editor, Static Analysis - 18th International Symposium, SAS 2011 , Venice, Italy, September 14--16, 2011. Proceedings, volume 6887 of LNCS , pages 369 -- 385 . Springer , 2011. ISBN 978--3--642--23701-0. D. Monniaux and L. Gonnord. Using bounded model checking to focus fixpoint iterations. In E. Yahav, editor, Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14--16, 2011. Proceedings, volume 6887 of LNCS, pages 369--385. Springer, 2011. ISBN 978--3--642--23701-0."},{"key":"e_1_3_2_1_41_1","unstructured":"J. C.\n      Peralta\n     and \n      J. P.\n      Gallagher\n  . \n  Convex hull abstractions in specialization of CLP programs\n  . In M. Leuschel editor LOPSTR volume \n  2664\n   of \n  LNCS pages \n  90\n  --\n  108\n  . \n  Springer 2002\n  . ISBN 3--540--40438--4.   J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In M. Leuschel editor LOPSTR volume 2664 of LNCS pages 90--108. Springer 2002. ISBN 3--540--40438--4."},{"key":"e_1_3_2_1_42_1","series-title":"LNCS","first-page":"613","volume-title":"J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.- K","author":"Pettorossi A.","year":"2000","unstructured":"A. Pettorossi and M. Proietti . Perfect model checking via unfold\/fold transformations . In J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.- K . Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors, Computational Logic, volume 1861 of LNCS , pages 613 -- 628 . Springer , 2000 . A. Pettorossi and M. Proietti. Perfect model checking via unfold\/fold transformations. In J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.- K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors, Computational Logic, volume 1861 of LNCS, pages 613--628. Springer, 2000."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"V. F.\n      Turchin\n    .\n  The use of metasystem transition in theorem proving and program optimization\n  . In J.W. de Bakker and J. van Leeuwen editors Automata Languages\n   and Programming 7th Colloquium Noordweijkerhout The Netherland July 14--18 1980 Proceedings volume \n  85\n   of \n  LNCS pages \n  645\n  --\n  657\n  . \n  Springer 1980. ISBN 3-540-10003-2. . URL http:\/\/dx.doi.org\/10.1007\/3-540-10003-2 105.     10.1007\/3-540-10003-2\nV. F. Turchin. The use of metasystem transition in theorem proving and program optimization. In J.W. de Bakker and J. van Leeuwen editors Automata Languages and Programming 7th Colloquium Noordweijkerhout The Netherland July 14--18 1980 Proceedings volume 85 of LNCS pages 645--657. Springer 1980. ISBN 3-540-10003-2. . URL http:\/\/dx.doi.org\/10.1007\/3-540-10003-2 105.","DOI":"10.1007\/3-540-10003-2"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Mumbai India","acronym":"POPL '15"},"container-title":["Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2678015.2682544","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2678015.2682544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:52Z","timestamp":1750227172000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2678015.2682544"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,13]]},"references-count":43,"alternative-id":["10.1145\/2678015.2682544","10.1145\/2678015"],"URL":"https:\/\/doi.org\/10.1145\/2678015.2682544","relation":{},"subject":[],"published":{"date-parts":[[2015,1,13]]},"assertion":[{"value":"2015-01-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}