Papaya: Global Typestate Analysis of Aliased Objects Extended Version

Mathias Jakobsen, Alice Ravier, Ornela Dardha

Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To avoid inconsistent object states, typestates…