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:
In general we have <benchmark-suite>/<tool>/<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.