A flexible (C)LP-based approach to the analysis of object-oriented programs

Méndez-Lojo, Mario and Navas, J. and Hermenegildo, Manuel V. (2008). A flexible (C)LP-based approach to the analysis of object-oriented programs. In: "17th International Symposium, LOPSTR 2007", August 23-24, 2007, Kongens Lyngby, Denmark. ISBN 978-3-540-78768-6.

Description

Title: A flexible (C)LP-based approach to the analysis of object-oriented programs
Author/s:
  • Méndez-Lojo, Mario
  • Navas, J.
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 17th International Symposium, LOPSTR 2007
Event Dates: August 23-24, 2007
Event Location: Kongens Lyngby, Denmark
Title of Book: Logic-Based Program Synthesis and Transformation
Date: 2008
ISBN: 978-3-540-78768-6
Volume: 4915
Subjects:
Faculty: Facultad de Informática (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 (910kB) | Preview

Abstract

Static analyses of object-oriented programs usually rely on intermediate representations that respect the original semantics while having a more uniform and basic syntax. Most of the work involving object-oriented languages and abstract interpretation usually omits the description of that language or just refers to the Control Flow Graph(CFG) it represents. However, this lack of formalization on one hand results in an absence of assurances regarding the correctness of the transformation and on the other it typically strongly couples the analysis to the source language. In this work we present a framework for analysis of object-oriented languages in which in a first phase we transform the input program into a representation based on Horn clauses. This allows on one hand proving the transformation correct attending to a simple condition and on the other being able to apply an existing analyzer for (constraint) logic programming to automatically derive a safe approximation of the semantics of the original program. The approach is flexible in the sense that the first phase decouples the analyzer from most languagedependent features, and correct because the set of Horn clauses returned by the transformation phase safely approximates the standard semantics of the input program. The resulting analysis is also reasonably scalable due to the use of mature, modular (C)LP-based analyzers. The overall approach allows us to report results for medium-sized programs.

More information

Item ID: 14319
DC Identifier: http://oa.upm.es/14319/
OAI Identifier: oai:oa.upm.es:14319
Official URL: http://link.springer.com/chapter/10.1007%2F978-3-540-78769-3_11?LI=true
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 19 Jan 2013 13:34
Last Modified: 21 Apr 2016 13:56
  • 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