Joaquín Arias, PhD Student, IMDEA Software Institute
In this talk we present the framework Failure Tabled Constraint Logic Programming by Interpolation, FTCLP (Gange et al. 2013), that, similarly to Tabled Constraint Logic Programming, TCLP (Codognet 1995; Chico et al. 2012), combines the benefits of constraints and tabling in Prolog. FTCLP learns from failed derivations in order to prune further derivations. This allows to compute interpolants rather than constraint projection (TCLP) for generation of reuse conditions. As a result this technique: can be used where projection is too expensive or does not exist; and speeds up the execution of programs with many redundant failed derivations. In the presence of infinite derivations due to recursive clauses, it uses iterative deepening search to terminate in more cases than the standard execution model of CLP. This framework is then applied to the verification of safety properties in C programs and the results are compared with Blast, HSF and Tracer. Finally, we describe some differences between FTCLP and TCLP.