{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:07:30Z","timestamp":1715645250953},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"unspecified","delay-in-days":86,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a new execution strategy for constraint logic programs called <jats:italic>Failure Tabled CLP<\/jats:italic>. Similarly to <jats:italic>Tabled CLP<\/jats:italic> our strategy records certain derivations in order to prune further derivations. However, our method only learns from <jats:italic>failed derivations<\/jats:italic>. This allows us to compute <jats:italic>interpolants<\/jats:italic> rather than <jats:italic>constraint projection<\/jats:italic> for generation of <jats:italic>reuse conditions<\/jats:italic>. As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.<\/jats:p>","DOI":"10.1017\/s1471068413000379","type":"journal-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T16:24:58Z","timestamp":1380126298000},"page":"593-607","source":"Crossref","is-referenced-by-count":5,"title":["Failure tabled constraint logic programming by interpolation"],"prefix":"10.1017","volume":"13","author":[{"given":"GRAEME","family":"GANGE","sequence":"first","affiliation":[]},{"given":"JORGE A.","family":"NAVAS","sequence":"additional","affiliation":[]},{"given":"PETER","family":"SCHACHTE","sequence":"additional","affiliation":[]},{"given":"HARALD","family":"S\u00d8NDERGAARD","sequence":"additional","affiliation":[]},{"given":"PETER J.","family":"STUCKEY","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"S1471068413000379_ref22","unstructured":"McMillan K. L. 2010. Lazy annotation for program testing and verification. In CAV, 104\u2013118."},{"key":"S1471068413000379_ref20","unstructured":"Jhala R. and McMillan K. L. 2006. A practical and complete approach to predicate refinement. In TACAS, 459\u2013473."},{"key":"S1471068413000379_ref17","doi-asserted-by":"crossref","unstructured":"Jaffar J. , Murali V. , Navas J. A. and Santosa A. E. 2012. TRACER: A symbolic execution tool for verification. In CAV, 758\u2013766.","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"S1471068413000379_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068413000379_ref14","unstructured":"Henzinger T. A. , Jhala R. , Majumdar R. and McMillan K. L. 2004. Abstractions from proofs. In POPL, 232\u2013244."},{"key":"S1471068413000379_ref13","unstructured":"Gupta A. , Popeea C. and Rybalchenko A. 2011b. Solving recursion-free Horn clauses over LI+UIF. In APLAS, 188\u2013203."},{"key":"S1471068413000379_ref6","unstructured":"Codognet P. 1995. A tabulation method for constraint logic programming. In Symposium and Exhibition on Industrial Applications of Prolog."},{"key":"S1471068413000379_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480898"},{"key":"S1471068413000379_ref5","unstructured":"Cimatti A. , Griggio A. and Sebastiani R. 2008. Efficient interpolant generation in satisfiability modulo theories. In TACAS, 397\u2013412."},{"key":"S1471068413000379_ref16","unstructured":"Jaffar J. and Lassez J. 1987. Constraint logic programming. In POPL, 111\u2013119."},{"key":"S1471068413000379_ref24","unstructured":"R\u00fcmmer P. , Hojjat H. and Kuncak V. 2013. Disjunctive interpolants for horn-clause verification. In CAV, 347\u2013363."},{"key":"S1471068413000379_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"S1471068413000379_ref4","unstructured":"Christ J. , Hoenicke J. and Nutz A. 2012. SMTInterpol: An interpolating SMT solver. In SPIN, 248\u2013254."},{"key":"S1471068413000379_ref12","unstructured":"Gupta A. , Popeea C. and Rybalchenko A. 2011a. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, 331\u2013344."},{"key":"S1471068413000379_ref10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190086","article-title":"A practical approach to satisfiability modulo linear integer arithmetic.","volume":"8","author":"Griggio","year":"2012","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"S1471068413000379_ref9","unstructured":"Grebenshchikov S. , Lopes N. P. , Popeea C. and Rybalchenko A. 2012. Synthesizing software verifiers from proof rules. In PLDI, 405\u2013416."},{"key":"S1471068413000379_ref18","unstructured":"Jaffar J. , Santosa A. E. and Voicu R. 2008. Efficient memoization for dynamic programming with ad-hoc constraints. In AAAI, 297\u2013303."},{"key":"S1471068413000379_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"S1471068413000379_ref3","unstructured":"Chico de Guzm\u00e1n P. , Carro M. , Hermenegildo M. V. and Stuckey P. J. 2012. A general implementation framework for tabled CLP. In FLOPS, 104\u2013119."},{"key":"S1471068413000379_ref19","unstructured":"Jaffar J. , Santosa A. E. and Voicu R. 2009. An interpolation method for CLP traversal. In CP, 454\u2013469."},{"key":"S1471068413000379_ref21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5625.001.0001","volume-title":"Introduction to Constraint Logic Programming","author":"Marriott","year":"1998"},{"key":"S1471068413000379_ref25","unstructured":"Tamaki H. and Sato T. 1986. OLD resolution with tabulation. In ICLP, 84\u201398."},{"key":"S1471068413000379_ref8","unstructured":"Graf S. and Sa\u00efdi H. 1997. Construction of abstract state graphs with pvs. In CAV, 72\u201383."},{"key":"S1471068413000379_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/131295.131299"},{"key":"S1471068413000379_ref23","unstructured":"McMillan K. L. 2011. Interpolants from z3 proofs. In FMCAD, 19\u201327."},{"key":"S1471068413000379_ref1","unstructured":"Angelis E. D. , Fioravanti F. , Proietti M. and Pettorossi A. 2012. Software model checking by program specialization. In CILC, 89\u2013103."}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068413000379","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T09:29:20Z","timestamp":1715592560000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068413000379\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":26,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S1471068413000379"],"URL":"https:\/\/doi.org\/10.1017\/s1471068413000379","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}