TY - JOUR
T1 - Automated verification of shape, size and bag properties via user-defined predicates in separation logic
AU - Chin, Wei-Ngan
AU - David, Cristina
AU - Nguyen, Huu Hai
AU - Qin, Shengchao
N1 - Author can archive post-print (ie final draft post-refereeing).
PY - 2012/8
Y1 - 2012/8
N2 - 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.
AB - 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.
U2 - 10.1016/j.scico.2010.07.004
DO - 10.1016/j.scico.2010.07.004
M3 - Article
SN - 0167-6423
VL - 77
SP - 1006
EP - 1036
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 9
ER -