Verification of semantic commutativity conditions and inverse operations on linked data structures
We present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantical...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2012
|
| Online Access: | http://hdl.handle.net/1721.1/72350 https://orcid.org/0000-0001-8195-4145 https://orcid.org/0000-0001-8095-8523 |