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

170 Downloads (Pure)


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
Publication statusPublished - 2007
Event12th IEEE International Conference on Engineering Complex Computer Systems - Auckland, New Zealand
Duration: 11 Jul 200714 Jul 2007


Conference12th IEEE International Conference on Engineering Complex Computer Systems
Abbreviated titleICECCS 2007
Country/TerritoryNew Zealand

Bibliographical note

Author can archive publisher's version/PDF.


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

Cite this