VCDryad extends the Vcc framework to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. The natural proof technique for heap verification provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic.


VCDryad was evaluated on more than 150 data-structure manipulating routines, which in turn exercised the natural proof technique for C for thousands of verification conditions. The programs were written with user-defined data structure definitions and annotated with preconditions, postconditions, and loop invariants. No further proof tactics were provided.

Comparison with related deductive verification frameworks

There are, in general, three layers of annotations common in current deductive verification tools:
  1. the specification, written as pre/post/assert annotations in code
  2. loop invariants and strengthening of pre/- post conditions that encode inductive invariants
  3. proof tactic advises from the user to the underlying prover to prove the resulting verification conditions

Annotations of type A that encode specifications are always required. Most current tools, like VeriFast, Bedrock, Vcc, and Dafny, require all three levels (A, B, and C) of annotations for proving code correct. The tool VCDryad presented in this paper and our previous tool requires A and B annotations only, relieving the programmer from writing annotations of type C, for data-structure verification.

The annotations encoding proof tactics (C) are clearly the hardest to write for a programmer, and typically require expertise in the workings of the underlying prover. Below we provide examples of these proof-tactic annotations in various tools and give an idea of the relief of burden provided by VCDryad.


Natural Proofs for Data Structure Manipulation in C using Separation Logic
To appear in Proc. 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14), 2014.