A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs

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 riented 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 t...

• Type: Conference
• Year: 2007
• Where: LOPSTR
• Authors: Mario Méndez-Lojo, Jorge Navas, Manuel V. Hermenegildo
• Keywords: Horn Clauses, Input Program, LOPSTR 2007, first Phase