Computing abstract distances in logic programs

DOI10.1007/978-3-030-45260-5_4MaRDI QIDQ5097625zbMATH OpenOpenAlexFDO

Authors Ignacio Casso, P. López-García, Roberto Giacobazzi, Manuel Hermenegildo, J. F. Morales

Publication date 25 August 2022

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1907.13263, http://oa.upm.es/63676/

zbMATH Keywords

abstract interpretationcomplete latticesdistanceslogic programmingmetricsprogram semanticsstatic analysis

Mathematics Subject Classification ID

Logic programming (68N17)

Abstract: Abstract interpretation is a well-established technique for performing static analyses of logic programs. However, choosing the abstract domain, widening, fixpoint, etc. that provides the best precision-cost trade-off remains an open problem. This is in a good part because of the challenges involved in measuring and comparing the precision of different analyses. We propose a new approach for measuring such precision, based on defining distances in abstract domains and extending them to distances between whole analyses of a given program, thus allowing comparing precision across different analyses. We survey and extend existing proposals for distances and metrics in lattices or abstract domains, and we propose metrics for some common domains used in logic program analysis, as well as extensions of those metrics to the space of whole program analysis. We implement those metrics within the CiaoPP framework and apply them to measure the precision of different analyses over both benchmarks and a realistic program.

Recommendations

• scientific article; zbMATH DE number 1973222
• Differential methods in logic program analysis
• Abstract interpretation and application to logic programs
• “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics
• Comparison of abstract interpretations

Cites work

• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A practical framework for theabstract interpretation of logic programs
• Analysis of Linear Hybrid Systems in CLP
• Comparison of abstract interpretations
• Efficient run-time type checking of typed logic programs
• Foundations of inductive logic programming
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 1615263 (Why is no real title available?)
• scientific article; zbMATH DE number 1181276 (Why is no real title available?)
• scientific article; zbMATH DE number 1973222 (Why is no real title available?)
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• Measures in Boolean Algebras
• Semantic code browsing
• SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities

Cited in

(4)

• Completeness of string analysis for dynamic languages
• Testing your (static analysis) truths
• scientific article; zbMATH DE number 7028386 (Why is no real title available?)
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs

This page was built for publication: Computing abstract distances in logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5097625)