No CrossRef data available.
Article contents
Failure tabled constraint logic programming by interpolation*
Published online by Cambridge University Press: 25 September 2013
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method only learns from failed derivations. This allows us to compute interpolants rather than constraint projection for generation of reuse conditions. 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.
Information
- Type
- Regular Papers
- Information
- Theory and Practice of Logic Programming , Volume 13 , Special Issue 4-5: 29th International Conference on Logic Programming , July 2013 , pp. 593 - 607
- Copyright
- Copyright © 2013 [GRAEME GANGE, JORGE A. NAVAS, PETER SCHACHTE, HARALD SØNDERGAARD and PETER J. STUCKEY]
Footnotes
*
We wish to thank Jose. F. Morales for providing support integrating MathSAT into Ciao and Manuel Carro and Corneliu Popeea for fruitful discussions about tabling and interpolation, respectively. We acknowledge support of the Australian Research Council through Discovery Project Grant DP110102579.
References
Angelis, E. D., Fioravanti, F., Proietti, M. and Pettorossi, A. 2012. Software model checking by program specialization. In CILC, 89–103.Google Scholar
Beyer, D., Henzinger, T., Jhala, R. and Majumdar, R. 2007. The software model checker BLAST. International Journal on Software Tools for Technology Transfer (STTT) 9, 505–525.CrossRefGoogle Scholar
Chico de Guzmán, P., Carro, M., Hermenegildo, M. V. and Stuckey, P. J. 2012. A general implementation framework for tabled CLP. In FLOPS, 104–119.Google Scholar
Christ, J., Hoenicke, J. and Nutz, A. 2012. SMTInterpol: An interpolating SMT solver. In SPIN, 248–254.CrossRefGoogle Scholar
Cimatti, A., Griggio, A. and Sebastiani, R. 2008. Efficient interpolant generation in satisfiability modulo theories. In TACAS, 397–412.Google Scholar
Codognet, P. 1995. A tabulation method for constraint logic programming. In Symposium and Exhibition on Industrial Applications of Prolog.Google Scholar
Craig, W. 1957. Linear reasoning: A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22, 3, 250–268.10.2307/2963593CrossRefGoogle Scholar
Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with pvs. In CAV, 72–83.Google Scholar
Grebenshchikov, S., Lopes, N. P., Popeea, C. and Rybalchenko, A. 2012. Synthesizing software verifiers from proof rules. In PLDI, 405–416.Google Scholar
Griggio, A. 2012. A practical approach to satisfiability modulo linear integer arithmetic. Journal on Satisfiability, Boolean Modeling and Computation 8, 1–27.CrossRefGoogle Scholar
Gulwani, S., Mehra, K. K. and Chilimbi, T. M. 2009. SPEED: Precise and efficient static estimation of program computational complexity. In POPL, 127–139.10.1145/1480881.1480898CrossRefGoogle Scholar
Gupta, A., Popeea, C. and Rybalchenko, A. 2011a. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, 331–344.Google Scholar
Gupta, A., Popeea, C. and Rybalchenko, A. 2011b. Solving recursion-free Horn clauses over LI+UIF. In APLAS, 188–203.Google Scholar
Henzinger, T. A., Jhala, R., Majumdar, R. and McMillan, K. L. 2004. Abstractions from proofs. In POPL, 232–244.Google Scholar
Hermenegildo, M. V., Bueno, F., Carro, M., López-García, P., Mera, E., Morales, J. F. and Puebla, G. 2012. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming 12, 1–2, 219–252.CrossRefGoogle Scholar
Jaffar, J., Murali, V., Navas, J. A. and Santosa, A. E. 2012. TRACER: A symbolic execution tool for verification. In CAV, 758–766.CrossRefGoogle Scholar
Jaffar, J., Santosa, A. E. and Voicu, R. 2008. Efficient memoization for dynamic programming with ad-hoc constraints. In AAAI, 297–303.Google Scholar
Jaffar, J., Santosa, A. E. and Voicu, R. 2009. An interpolation method for CLP traversal. In CP, 454–469.Google Scholar
Jhala, R. and McMillan, K. L. 2006. A practical and complete approach to predicate refinement. In TACAS, 459–473.Google Scholar
Marriott, K. and Stuckey, P. J. 1998. Introduction to Constraint Logic Programming. MIT Press, Cambridge, MA, USA.CrossRefGoogle Scholar
McMillan, K. L. 2010. Lazy annotation for program testing and verification. In CAV, 104–118.Google Scholar
Rümmer, P., Hojjat, H. and Kuncak, V. 2013. Disjunctive interpolants for horn-clause verification. In CAV, 347–363.Google Scholar
Warren, D. S. 1992. Memoing for logic programs. Communcations of the ACM 35, 3, 93–111.10.1145/131295.131299CrossRefGoogle Scholar
Gange supplementary material
Gange supplementary material
PDF
73.1 KB
You have
Access
- 5
- Cited by