VACID solutions

This codeplex project is used to keep track of various attempts at solving verification problems:

• posed in a paper VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0 PDF
• possibly others in future

The directory structure is:

VACID-0/
   Dafny/
      README.txt
      Composite.dfy
      SparseArray.dfy
      ...
   VCC/
      README.txt
      SparseArray.c
      ...

In general we have <benchmark-suite>/<tool>/<benchmark>. <benchmark> might be a directory or a file depending on the tool.

We currently only have VACID-0 solutions. If you want to contribute your solutions, please contact Michał Moskal or Rustan Leino about source control access and then create a directory for your tool under VACID-0/.

Copyright for solutions remains with authors, but all solutions are required to be licensed under a BSD license.