Export or edit this event...

Jonathan Aldrich: Typestate Verification for Aliased Objects using Assume-Guarantee Permissions

Portland State University Engineering Building
1930 SW 4th Ave
Portland, Oregon 97201, US (map)



We are having a special summer colloquium presentation by Jonathan Aldrich of CMU on Tuesday, August 12, at 10:30am. Title and abstract below.

The talk will be in the Dean's Conference room (EB 500) in the Engineering Building at Portland State University.

Jim Hook (hook at cs dot pdx dot edu) is acting as host.

TITLE: Typestate Verification for Aliased Objects using Assume-Guarantee Permissions

ABSTRACT: 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 assume- guarantee permissions. These permissions track not only the state of an object, but an abstraction of what operations other aliases might perform on the object. 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 describe novel approaches for reasoning about inheritance and concurrency, and show case studies verifying code (and finding one defect) in well-tested Java standard library code.

This is joint work with Kevin Bierhoff and Nels Beckman.