CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Seminars @ CITI  \  Seminar Page Login  
banner bottom
File Top
Typestate Verification for Aliased Objects using Invariant-Carrying Permissions
{ Tue, 14 Jul 2009, 14h00 }

By: Jonathan Aldrich  [ show info ]

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.

Hosted by: Software Systems

Location: DI Seminars Room

File Bottom