W.N. Chin
Automated Verification of Shape, Size and Bag Properties
Chin, W.N.; David, C.; Nguyen, H.H.; Qin, S.
Authors
C. David
H.H. Nguyen
S. Qin
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 (multi-set) 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.
Citation
Chin, W., David, C., Nguyen, H., & Qin, S. (2007). Automated Verification of Shape, Size and Bag Properties. In 12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings (307-320). https://doi.org/10.1109/iceccs.2007.17
Conference Name | 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007) |
---|---|
Conference Location | Auckland, New Zealand |
Start Date | Jul 11, 2007 |
End Date | Jul 14, 2007 |
Publication Date | Jul 1, 2007 |
Deposit Date | Nov 17, 2009 |
Publicly Available Date | Mar 28, 2024 |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 307-320 |
Book Title | 12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings. |
DOI | https://doi.org/10.1109/iceccs.2007.17 |
Files
Published Conference Proceeding
(183 Kb)
PDF
Copyright Statement
© 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search