Accumulation Analysis

Martin Kellogg, Narges Shadab, Manu Sridharan, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


A typestate specification indicates which behaviors of an object are permitted in each of the object's states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.

Original languageEnglish (US)
Title of host publication36th European Conference on Object-Oriented Programming, ECOOP 2022
EditorsKarim Ali, Jan Vitek
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772259
StatePublished - Jun 1 2022
Externally publishedYes
Event36th European Conference on Object-Oriented Programming, ECOOP 2022 - Berlin, Germany
Duration: Jun 6 2022Jun 10 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference36th European Conference on Object-Oriented Programming, ECOOP 2022

All Science Journal Classification (ASJC) codes

  • Software


  • Typestate
  • finite-state property


Dive into the research topics of 'Accumulation Analysis'. Together they form a unique fingerprint.

Cite this