Please use this identifier to cite or link to this item: https://doi.org/10.1016/j.scico.2010.07.004
Title: Automated verification of shape, size and bag properties via user-defined predicates in separation logic
Authors: Chin, W.-N. 
David, C.
Nguyen, H.H. 
Qin, S.
Keywords: Automated verification
Entailment checking
Inductive shape predicates with size and bag properties
Separation logic
Issue Date: 2012
Source: Chin, W.-N., David, C., Nguyen, H.H., Qin, S. (2012). Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming 77 (9) : 1006-1036. ScholarBank@NUS Repository. https://doi.org/10.1016/j.scico.2010.07.004
Abstract: Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this paper, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach. © 2011 Elsevier B.V. All rights reserved.
Source Title: Science of Computer Programming
URI: http://scholarbank.nus.edu.sg/handle/10635/42335
ISSN: 01676423
DOI: 10.1016/j.scico.2010.07.004
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

64
checked on Dec 13, 2017

WEB OF SCIENCETM
Citations

27
checked on Dec 13, 2017

Page view(s)

100
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.