with contributions from
Andrew W. Appel, Lennart Beringer, Robert Dockins, Josiah Dodds, Aquinas Hobor, Jean-Marie Madiot, Gordon Stewart, Qinxiang Cao, and others.
The LICENSE file has information about copyright, licensing, and permissions.
Our webpage describes the goals of the project and has links to many related publications.
For an introduction to how to use Verifiable C, read the manual, which has tutorial case studies.
Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014. Available in hardcover or e-book PDF.
See the file BUILD_ORGANIZATION for an explanation of how to build and install the VST.