Verified Software Toolchain
Coq C Verilog OCaml TeX Makefile Other
Permalink
Failed to load latest commit information.
aes More porting. Jul 10, 2018
compcert Remove many unused .v files in sepcomp directory; Jul 12, 2018
concurrency Moving the void_extspec definition into veric. Jul 18, 2018
doc Remove a redundant line in progs/funcptr.c. That was a infelicity bef… Jul 12, 2018
examples msl ported + cleaning trailing spaces Jan 13, 2017
fcf Remove the unnecessary ccc26x86 directory, Jul 6, 2018
floyd Improve forward_for_simple_bound. Jul 22, 2018
hmacdrbg Tiny edits. Jul 16, 2018
hmacfcf msl ported + cleaning trailing spaces Jan 13, 2017
mailbox Fix a bug. Jul 16, 2018
mc_reify Qualified path names now start with VST.floyd, VST.veric, etc., Aug 15, 2017
msl Improve tactic build_func_abs_right to generate function abstraction … Jul 10, 2018
progs Merge pull request #265 from PrincetonUniversity/small-fix Jul 21, 2018
sepcomp Remove many unused .v files in sepcomp directory; Jul 12, 2018
sha Fix some bugs in new forward_for_simple_bound. Some proofs in our exa… Jul 9, 2018
tweetnacl20140427 Improve another proof. Jul 16, 2018
util Put the -Q flags back the way they were, because Proof General Jul 3, 2018
veric Moving the void_extspec definition into veric. Jul 18, 2018
veristar Fix tactic level mistake about (assert_PROP + by) etc. May 31, 2018
wand Adjust the port to CompCert 3.3 by removing unnecessary (and not-open… Jun 28, 2018
wand_demo Adjust the port to CompCert 3.3 by removing unnecessary (and not-open… Jun 28, 2018
.gitattributes Adjusted .travis.yml to record Coq version and Git commit date. Nov 29, 2017
.gitignore Suddenly find that two different links (one was wrong) appear in our … Feb 6, 2018
.travis.yml Try coq88 on travis. Jul 16, 2018
BUILD_ORGANIZATION.md Got rid of .loadpath, now we use only _CoqProject Apr 30, 2018
CHANGES 1. start_function now chooses good names for lvar and gvar LOCAL defs, Oct 4, 2017
HISTORY msl ported + cleaning trailing spaces Jan 13, 2017
LICENSE msl ported + cleaning trailing spaces Jan 13, 2017
Makefile Try to solve #262. Only a start. Jul 21, 2018
README.md Tweaked the readme Jan 17, 2018
VERSION 1. In floyd/proofauto, Require msl/iter_sepcon, msl/wand_frame, msl/w… May 17, 2018
archive-unused msl ported + cleaning trailing spaces Jan 13, 2017
pg msl ported + cleaning trailing spaces Jan 13, 2017

README.md

Verified Software Toolchain

with contributions from

Andrew W. Appel, Lennart Beringer, Robert Dockins, Josiah Dodds, Aquinas Hobor, Gordon Stewart, Qinxiang Cao, and others.

The LICENSE file has information about copyright, licensing, and permissions.

Documentation:

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.

Build:

See the file BUILD_ORGANIZATION for an explanation of how to build and install the VST.