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 | 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. 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.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.