Natural proofs for structure, data, and separation

Xiaokang Qiu, Pranav Garg, Andrei Ştefanescu, Madhusudan Parthasarathy

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

Abstract

We propose natural proofs for reasoning with programs that manipulate data-structures against specifications that describe the structure of the heap, the data stored within it, and separation and framing of sub-structures. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, that provide sound but incomplete procedures, and that capture common reasoning tactics in program verification. We develop a dialect of separation logic over heaps, called Dryad, with recursive definitions that avoids explicit quantification. We develop ways to reason with heaplets using classical logic over the theory of sets, and develop natural proofs for reasoning using proof tactics involving disciplined unfoldings and formula abstractions. Natural proofs are encoded into decidable theories of first-order logic so as to be discharged using SMT solvers. We also implement the technique and show that a large class of more than 100 correct programs that manipulate data-structures are amenable to full functional correctness using the proposed natural proof method. These programs are drawn from a variety of sources including standard data-structures, the Schorr-Waite algorithm for garbage collection, a large number of low-level C routines from the Glib library and OpenBSD library, the Linux kernel, and routines from a secure verified OS-browser project. Our work is the first that we know of that can handle such a wide range of full functional verification properties of heaps automatically, given pre/post and loop invariant annotations. We believe that this work paves the way for deductive verification technology to be used by programmers who do not (and need not) understand the internals of the underlying logic solvers, significantly increasing their applicability in building reliable systems.

Original languageEnglish (US)
Title of host publicationPLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages231-242
Number of pages12
DOIs
StatePublished - Sep 2 2013
Event34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013 - Seattle, WA, United States
Duration: Jun 16 2013Jun 19 2013

Publication series

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

Other

Other34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013
Country/TerritoryUnited States
CitySeattle, WA
Period6/16/136/19/13

Keywords

  • Data structures
  • Heap analysis
  • Natural proofs
  • SMT solvers
  • Separation logic

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Natural proofs for structure, data, and separation'. Together they form a unique fingerprint.

Cite this