2019/07/31 by Joaquín Arias, Arias, Joaquin, Manuel Carro +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1908.00104
openalex publication_date 2019/07/31 · openalex created_date 2022/07/28 · openalex updated_date 2026/07/28
CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao\nProlog system. It includes PLAI, a fixpoint algorithm for the abstract\ninterpretation of logic programs which we adapt to use tabled constraint logic\nprogramming. In this adaptation, the tabling engine drives the fixpoint\ncomputation, while the constraint solver handles the LUB of the abstract\nsubstitutions of different clauses. That simplifies the code and improves\nperformance, since termination, dependencies, and some crucial operations\n(e.g., branch switching and resumption) are directly handled by the tabling\nengine. Determining whether the fixpoint has been reached uses semantic\nequivalence, which can decide that two syntactically different abstract\nsubstitutions represent the same element in the abstract domain. Therefore, the\ntabling analyzer can reuse answers in more cases than an analyzer using\nsyntactical equality. This helps achieve better performance, even taking into\naccount the additional cost associated to these checks. Our implementation is\nbased on the TCLP framework available in Ciao Prolog and is one-third the size\nof the initial fixpoint implementation in CiaoPP. Its performance has been\nevaluated by analyzing several programs using different abstract domains. This\npaper is under consideration for publication in Theory and Practice of Logic\nProgramming (TPLP).\n