CPA-SEL: Practical Typestate Verification with Assume-Guarantee Reasoning

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

CCF-0811592 CPA-SEL: Practical Typestate Verification with Assume-Guarantee Reasoning Jonathan Aldrich One of the main difficulties in modern software development is using software libraries and frameworks correctly. This project is developing new tools to verify temporal usage properties of libraries and frameworks, capturing the permitted ordering of calls to an object and the state of that object when the calls are made. Key verification challenges addressed by this project include inheritance and subtyping, recursive callbacks from a library into the client and back, and multiple aliased pointers to a library object. The project is applying assume-guarantee reasoning to these challenges: allowing multiple clients to access an object cooperatively, with an agreement about how that object should be used so that each client can safely make assumptions about other clients? behavior, and in turn each client guarantees that it will not violate other clients? assumptions. The project is developing the underlying theory behind the approach, but is also building practical tools and evaluating them on real-world applications and libraries through scientific case studies. If successful, the project will increase the productivity of software engineers when using libraries, reduce the number of defects in software, and help students to learn about the theory and practice of lightweight software verification tools.