Please use this identifier to cite or link to this item:
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
Citation: 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.
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
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.


checked on Jun 25, 2022


checked on Jun 17, 2022

Page view(s)

checked on Jun 23, 2022

Google ScholarTM



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