Verification of Semantic Commutativity Conditions and Inverse Operations on Linked Data Structures

Download Now Date Added: Jun 2011
Format: PDF

The authors present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because their technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not necessarily identical) data structure states in different execution orders. They have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList).