Detail

Typestate Verification for Aliased Objects using Invariant-Carrying Permissions

Object-oriented libraries often define usage protocols that clients must follow in order for the system to work properly. Typestates use state machines to specify these protocols, but previous protocol verification systems have significant practical problems in their precision, scaleability, easy of use, and applicability to standard coding styles and idioms.

We are exploring a new approach to verifying typestate using invariant-carrying permissions. These permissions track not only the state of an object, but an abstraction of what operations other aliases might perform on the object and what invariants must remain true. Developers annotate their code with state and permission information, which can be automatically and soundly checked for consistency. Our approach is fully modular, yet allows substantial reasoning about objects even when they are aliased by multiple clients. We will briefly describe an application to concurrency, and show case studies verifying well-tested Java standard library code.

This is joint work with Kevin Bierhoff and Nels Beckman.