Sciweavers

Share
ICECCS
2007
IEEE

Automated Verification of Shape, Size and Bag Properties

9 years 6 months ago
Automated Verification of Shape, Size and Bag Properties
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.
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, She
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where ICECCS
Authors Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
Comments (0)
books