Automated Verification of Shape, Size and Bag Properties

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

125 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings IEEE international conference on engineering complex computer systems
Place of PublicationCalifornia
PublisherIEEE
Pages307-317
DOIs
Publication statusPublished - 2007
Event12th IEEE International Conference on Engineering Complex Computer Systems - Auckland, New Zealand
Duration: 11 Jul 200714 Jul 2007

Conference

Conference12th IEEE International Conference on Engineering Complex Computer Systems
Abbreviated titleICECCS 2007
CountryNew Zealand
CityAuckland
Period11/07/0714/07/07

Bibliographical note

Author can archive publisher's version/PDF.

Fingerprint Dive into the research topics of 'Automated Verification of Shape, Size and Bag Properties'. Together they form a unique fingerprint.

  • Cite this

    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