TY - JOUR
T1 - Verification of Snapshotable Trees using Access Permissions and Typestate
AU - Mehnert, Hannes
AU - Aldrich, Jonathan
PY - 2012
Y1 - 2012
N2 - We use access permissions and typestate to specify and ver- ify 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 verify- ing 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.
AB - We use access permissions and typestate to specify and ver- ify 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 verify- ing 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.
U2 - 10.1007/978-3-642-30561-0_14
DO - 10.1007/978-3-642-30561-0_14
M3 - Journal article
SN - 0302-9743
VL - 7304
SP - 187
EP - 201
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
ER -