Using program transformation, annotation, and reflection to certify a java type resolution function

Victor L. Winter, Carl Reinke, Jonathan Guerrero

Research output: Contribution to conferencePaperpeer-review

Abstract

In Java, type resolution is a function that takes a reference to a type occurring in a given context as input, and returns the canonical form of that type. This information is fundamental to static analysis - a 'must have' function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle.

Original languageEnglish (US)
Pages137-145
Number of pages9
DOIs
StatePublished - 2014
Event2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 - Miami, FL, United States
Duration: Jan 9 2014Jan 11 2014

Conference

Conference2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014
CountryUnited States
CityMiami, FL
Period1/9/141/11/14

Keywords

  • Annotation
  • Java
  • Program transformation
  • Reflection
  • Source code analysis
  • Type resolution

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Using program transformation, annotation, and reflection to certify a java type resolution function'. Together they form a unique fingerprint.

Cite this