A Constraint-Based Verification Approach for Java Bytecode Programs

Abstract

In this paper, we propose a constraint based analysis technique to detect theinconsistencies between a Java application and its specification at the Bytecode level. Themain objective of our approach is not only to exploit the information of the userspecification but also the memory constraints generated from the Java Bytecode of theapplication. Indeed, this allows us to detect the possible non-conformance between aprogram and its specification and also to explore the execution paths of the applicationlooking at which of them may contain such inconsistencies. Nevertheless, the testingapplication and the user specification are not in the same level of abstraction. Thereby,we propose to wrap the method under test with its specification expressed as pre/postspecifications at the Bytecode level, using the Static Bytecode Instrumentation.