- Example execution
- executable semantics (maybe in K)
- investigate compiler correctness either to CPM or sequential program
with contributions from
Andrew W. Appel, Lennart Beringer, Robert Dockins, Josiah Dodds, Aquinas Hobor, Jean-Marie Madiot, Gordon Stewart, Qinxiang Cao, Qinshi Wang, 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, or consult Software Foundations Volume 5: Verifiable C for a tutorial with exercises.
Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014. Available in hardcover.