Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/41337
Title: Automated verification of shape and size properties via separation logic
Authors: Nguyen, H.H.
David, C.
Qin, S.
Chin, W.-N. 
Issue Date: 2007
Source: Nguyen, H.H.,David, C.,Qin, S.,Chin, W.-N. (2007). Automated verification of shape and size properties via separation logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4349 LNCS : 251-266. ScholarBank@NUS Repository.
Abstract: Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system. © Springer-Verlag Berlin Heidelberg 2007.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/41337
ISBN: 3540697357
ISSN: 03029743
Appears in Collections:Staff Publications

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

Page view(s)

60
checked on Dec 16, 2017

Google ScholarTM

Check


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