In recent years, separation logic has emerged as a contender for formal reasoning of heap-manipulating imperative programs. Recent works have focused on specialised provers that are mostly based on fixed sets of predicates. To improve expressivity, we have proposed a prover that can automatically handle user-defined predicates. These shape predicates allow programmers to describe a wide range of data structures with their associated size properties. In the current work, we shall enhance this prover by providing support for a new type of constraints, namely bag (multiset) constraints. With this extension, we can capture the reachable nodes (or values) inside a heap predicate as a bag constraint. Consequently, we are able to prove properties about the actual values stored inside a data structure.
|Title of host publication||Proceedings IEEE international conference on engineering complex computer systems|
|Place of Publication||California|
|Publication status||Published - 2007|
|Event||12th IEEE International Conference on Engineering Complex Computer Systems - Auckland, New Zealand|
Duration: 11 Jul 2007 → 14 Jul 2007
|Conference||12th IEEE International Conference on Engineering Complex Computer Systems|
|Abbreviated title||ICECCS 2007|
|Period||11/07/07 → 14/07/07|
Bibliographical noteAuthor can archive publisher's version/PDF.
Chin, W-N., David, C., Nguyen, H. H., & Qin, S. (2007). Automated Verification of Shape, Size and Bag Properties. In Proceedings IEEE international conference on engineering complex computer systems (pp. 307-317). IEEE. https://doi.org/10.1109/ICECCS.2007.17