Automated Verification of Shape, Size and Bag Properties

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

doi:10.1109/ICECCS.2007.17

Automated Verification of Shape, Size and Bag Properties

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

SCEDT School Executive Team

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

272 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 language	English
Title of host publication	Proceedings IEEE international conference on engineering complex computer systems
Place of Publication	California
Publisher	IEEE
Pages	307-317
DOIs	https://doi.org/10.1109/ICECCS.2007.17
Publication status	Published - 2007
Event	12th IEEE International Conference on Engineering Complex Computer Systems - Auckland, New Zealand Duration: 11 Jul 2007 → 14 Jul 2007

Conference

Conference	12th IEEE International Conference on Engineering Complex Computer Systems
Abbreviated title	ICECCS 2007
Country/Territory	New Zealand
City	Auckland
Period	11/07/07 → 14/07/07

Bibliographical note

Author can archive publisher's version/PDF.

Access to Document

10.1109/ICECCS.2007.17

Full textFinal published version, 266 KBLicence: CC BY-NC-ND

http://ieeexplore.ieee.org/document/4276328/

Cite this

@inproceedings{8ba22ba141cd4b41b41a00f87ce9a651,

title = "Automated Verification of Shape, Size and Bag Properties",

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.",

author = "Wei-Ngan Chin and Cristina David and Nguyen, \{Huu Hai\} and Shengchao Qin",

note = "Author can archive publisher's version/PDF. ; 12th IEEE International Conference on Engineering Complex Computer Systems, ICECCS 2007 ; Conference date: 11-07-2007 Through 14-07-2007",

year = "2007",

doi = "10.1109/ICECCS.2007.17",

language = "English",

pages = "307--317",

booktitle = "Proceedings IEEE international conference on engineering complex computer systems",

publisher = "IEEE",

}

TY - GEN

T1 - Automated Verification of Shape, Size and Bag Properties

AU - Chin, Wei-Ngan

AU - David, Cristina

AU - Nguyen, Huu Hai

AU - Qin, Shengchao

N1 - Author can archive publisher's version/PDF.

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1109/ICECCS.2007.17

DO - 10.1109/ICECCS.2007.17

M3 - Conference contribution

SP - 307

EP - 317

BT - Proceedings IEEE international conference on engineering complex computer systems

PB - IEEE

CY - California

T2 - 12th IEEE International Conference on Engineering Complex Computer Systems

Y2 - 11 July 2007 through 14 July 2007

ER -

Automated Verification of Shape, Size and Bag Properties

Abstract

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this