VCDryad

Automated deductive verification framework

About

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.

Evaluation

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.

• VCDryad vs Vcc
  Vcc does not support separation logic, and hence even the specification is complex and very hard to write. Also, Vcc requires hints using assertions, without which it would not be able to prove the loop invariants. VCDryad allows for more succinct separation logic specifications and does not need any additional guidance in terms of proof tactics.
• VCDryad vs VeriFast
  Verification of the bst insertion procedure in VeriFast relies on user’s help in form of annotations at particular program locations to unbundle (open) heaplets and re-bundle (close) heaplets, as well as three user provided lemmas. Moreover, the user also needs to manually instantiate a lemma to finalize the proof. The verification using VCDryad of the same procedure requires no annotations for helping proofs.
• VCDryad vs Bedrock
  Bedrock and VCDryad versions do not prove exactly the same property because Bedrock uses Coq's list type family to abstractly represent memory location while VCDryad reasons about list structure and set of keys stored in the list. However, Bedrock does require hints to be provided by the user; user-provided administrative lemmas for each separation logic predicate, to relate memory representation to abstract representation using four more lemmas that are need to be packaged together using a Bedrock tactic. No such user intervention is needed to prove C version using VCDryad.

Publications

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.

People

• Edgar Pek
• Xiaokang Qiu
• P. Madhusudan