Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Heap monotonic typestate

Manuel Fähndrich and K. Rustan M. Leino


The paper defines the class of heap monotonic typestates. The monotonicity of such typestates enables sound checking algorithms without the need for non-aliasing regimes of pointers. The basic idea is that data structures evolve over time in a manner that only makes their representation invariants grow stronger, never weaker. This assumption guarantees that existing object references with particular typestates remain valid in all program futures, while still allowing objects to attain new stronger typestates. The system is powerful enough to establish properties of circular data structures.


Publication typeInproceedings
Published inProceedings of the first International Workshop on Alias Confinement and Ownership (IWACO)
> Publications > Heap monotonic typestate