Please use this identifier to cite or link to this item:
https://doi.org/10.1109/ICECCS.2007.17
Title: | Automated verification of shape, size and bag properties | Authors: | Chin, W.-N. David, C. Nguyen, H.H. Qin, S. |
Issue Date: | 2007 | Citation: | Chin, W.-N., David, C., Nguyen, H.H., Qin, S. (2007). Automated verification of shape, size and bag properties. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS : 307-317. ScholarBank@NUS Repository. https://doi.org/10.1109/ICECCS.2007.17 | Abstract: | 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. © 2007 IEEE. | Source Title: | Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS | URI: | http://scholarbank.nus.edu.sg/handle/10635/40463 | ISBN: | 0769528953 | DOI: | 10.1109/ICECCS.2007.17 |
Appears in Collections: | Staff Publications |
Show full item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.