Natural proofs for data structure manipulation in C using separation logic

Edgar Pek, Xiaokang Qiu, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationPLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation
PublisherAssociation for Computing Machinery
Pages440-451
Number of pages12
ISBN (Print)9781450327848
DOIs
StatePublished - 2014
Event35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014 - Edinburgh, United Kingdom
Duration: Jun 9 2014Jun 11 2014

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014
CountryUnited Kingdom
CityEdinburgh
Period6/9/146/11/14

Keywords

  • Data structures
  • Natural proofs
  • Program verifiers
  • Separation logic

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Natural proofs for data structure manipulation in C using separation logic'. Together they form a unique fingerprint.

Cite this