Verification of Java Bytecode Using Analysis and Transformation of Logic Programs
Source: Cornell University
State of the art analyzers in the Logic Programming (LP) paradigm are nowadays mature and sophisticated. They allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. The aim of this paper is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (jvml). In order to achieve the authors' goal, the authors rely on well-known techniques for meta-programming and program specialization. More precisely, they propose to partially evaluate a jvml interpreter implemented in LP together with (an LP representation of) a jvml program and then analyze the residual program.