Certifying a java type resolution function using program transformation, annotation, and reflection

Victor Winter, Carl Reinke, Jonathan Guerrero

Research output: Contribution to journalArticlepeer-review


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 name 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)
Pages (from-to)115-135
Number of pages21
JournalSoftware Quality Journal
Issue number1
StatePublished - Mar 1 2016


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

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


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

Cite this