Substructural typestates
Filipe Militão, Jonathan Aldrich, Luı́s Caires · 2014
Finding simple, yet expressive, verification techniques to reason about both aliasing and mutable state has been a major challenge for static program verification. One such approach, of practical relevance, is centered around a lightweight typing discipline where types denote abstract object states, known as typestates.