Verifying pointer and string analyses with region type systems

Lennart Beringer, Robert Grabowski, Martin Hofmann

Research output: Contribution to journalArticlepeer-review

6 Scopus citations


Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and usually contributes to other analyses or code optimizations. In recent years, a number of algorithms have been presented that provide an efficient, scalable, and yet precise pointer analysis. However, it is unclear how the results of these algorithms compare to each other semantically. In this paper, we present a general region type system for a Java-like language and give a formal soundness proof. The system is subsequently specialized to obtain a platform for embedding the results of various existing context-sensitive pointer analysis algorithms, thereby equipping the computed relations with a common interpretation and verification. We illustrate our system by outlining an extension to a string value analysis that builds on pointer information.

Original languageEnglish (US)
Pages (from-to)49-65
Number of pages17
JournalComputer Languages, Systems and Structures
Issue number2
StatePublished - Jul 2013

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications


  • Formal verification
  • Object-oriented languages
  • Pointer alias analysis
  • Region type system
  • String analysis


Dive into the research topics of 'Verifying pointer and string analyses with region type systems'. Together they form a unique fingerprint.

Cite this