file.pdf (227.04 kB)
Verification of Snapshotable Trees using Access Permissions and Typestate
journal contribution
posted on 2012-05-01, 00:00 authored by Hannes Mehnert, Jonathan AldrichWe 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.