TY - GEN
T1 - Natural proofs for data structure manipulation in C using separation logic
AU - Pek, Edgar
AU - Qiu, Xiaokang
AU - Madhusudan, P.
N1 - Copyright:
Copyright 2014 Elsevier B.V., All rights reserved.
PY - 2014
Y1 - 2014
N2 - The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32]. In this work, we develop a framework called VCDRYAD that extends the VCC framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing VCC framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing VCC to find natural proofs using primarily decidable theories. We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, wellknown open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without any user-provided proof tactics. VCDRYAD is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
AB - The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32]. In this work, we develop a framework called VCDRYAD that extends the VCC framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing VCC framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing VCC to find natural proofs using primarily decidable theories. We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, wellknown open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without any user-provided proof tactics. VCDRYAD is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
KW - Data structures
KW - Natural proofs
KW - Program verifiers
KW - Separation logic
UR - http://www.scopus.com/inward/record.url?scp=84901611540&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84901611540&partnerID=8YFLogxK
U2 - 10.1145/2594291.2594325
DO - 10.1145/2594291.2594325
M3 - Conference contribution
AN - SCOPUS:84901611540
SN - 9781450327848
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 440
EP - 451
BT - PLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation
PB - Association for Computing Machinery
T2 - 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014
Y2 - 9 June 2014 through 11 June 2014
ER -