file.pdf (227.04 kB)

Verification of Snapshotable Trees using Access Permissions and Typestate

Download (227.04 kB)
journal contribution
posted on 01.05.2012 by Hannes Mehnert, Jonathan Aldrich

We use access permissions and typestate to specify and verify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe the challenges to verifying snapshotable trees in Plural, give an abstract interface specification against which we verify the client code, provide a concrete specification for an implementation and describe proof patterns we found. We also relate this verification approach to other techniques used to verify this data structure.

History

Publisher Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-30561-0_14

Date

01/05/2012

Exports

Exports