A formal design of a tool for static analysis of upper bounds on object calls in Java

Abstract. This paper presents a formal design of a tool for statically establishing the upper bound on the number of executions of objects’ methods in a fragment of object-oriented code. The algorithm that our tool employs is a multi-pass interprocedural analysis consisting of data flow and region-based analyses. We describe the formalization of each of stage of the algorithm. This rigorous specification greatly aids the implementation of the tool by removing ambiguities of textual descrip-tions. There are many applications for information obtained through this method including reasoning about concurrent code, scheduling, code optimization, compositing services, etc.We concentrate on using upper bounds to instrument transactional code that uses a synchronization mechanism based on versioning, and therefore benefits from a priori knowledge about the usage of shared objects within each transaction. To this end we implement a precompiler for Java that analyzes transac-tions, and injects generated source code to initialize each transaction