Incremental analysis of logic programs with assertions and open predicates

García Contreras, Isabel and Morales Caballero, José Francisco and Hermenegildo, Manuel V. (2019). Incremental analysis of logic programs with assertions and open predicates. In: "Logic-Based Program Synthesis and Transformation". Lecture Notes in Computer Science (12042). Springer, Suiza, pp. 36-56. ISBN 978-3-030-45259-9. https://doi.org/10.1007/978-3-030-45260-5.

Description

Title: Incremental analysis of logic programs with assertions and open predicates
Author/s:
  • García Contreras, Isabel
  • Morales Caballero, José Francisco
  • Hermenegildo, Manuel V.
Item Type: Book Section
Title of Book: Logic-Based Program Synthesis and Transformation
Date: 2019
ISBN: 978-3-030-45259-9
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

Generic components are a further abstraction over the concept of modules, introducing dependencies on other (not necessarily available) components implementing specified interfaces. They have become a key concept in large and complex software applications. Despite undeniable advantages, generic code is also anti-modular. Precise analysis (e.g., for detecting bugs or optimizing code) requires such code to be instantiated with concrete implementations, potentially leading to expensive combinatorial explosion. In this paper we claim that incremental, whole program analysis can be very beneficial in this context, and alleviate the anti-modularity nature of generic code. We propose a simple Horn-clause encoding of generic programs, using open predicates and assertions, and we introduce a new incremental, multivariant analysis algorithm that reacts incrementally not only to changes in program clauses, but also to changes in the assertions, upon which large parts of the analysis graph may depend. We also discuss the application of the proposed techniques in a number of practical use cases. In addition, as a realistic case study, we apply the proposed techniques in the analysis of the LPdoc documentation system. We argue that the proposed traits are a convenient and elegant abstraction for modular generic programming, and that our preliminary results support our thesis that the new incrementality-related features added to the analysis bring promising advantages in this context.

Funding Projects

TypeCodeAcronymLeaderTitle
Government of SpainTIN2015-67522-C3-1-RTRACESFundación IMDEA SoftwareTecnologías y herramientas para el desarrollo de software consciente de los recursos, correcto y eficiente (IMDEA)
Government of SpainFPU16/04811UnspecifiedUnspecifiedUnspecified
Madrid Regional GovernmentP2018/TCS-4339BLOQUES-CMUnspecifiedContratos inteligentes y blockchains escalables y seguros mediante verificación y análisis

More information

Item ID: 63681
DC Identifier: http://oa.upm.es/63681/
OAI Identifier: oai:oa.upm.es:63681
DOI: 10.1007/978-3-030-45260-5
Official URL: https://link.springer.com/chapter/10.1007/978-3-030-45260-5_3
Deposited by: Memoria Investigacion
Deposited on: 15 Oct 2020 06:54
Last Modified: 15 Oct 2020 06:54
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM