Skip to content

PrincetonUniversity/VST

Folders and files

NameName
Last commit message
Last commit date
Jan 7, 2025
Jan 8, 2025
Jul 24, 2024
Jul 24, 2024
Sep 19, 2024
Jun 30, 2023
Jul 25, 2024
Apr 1, 2023
Jan 31, 2023
Dec 20, 2022
Jan 8, 2025
Aug 8, 2024
Jul 26, 2024
May 26, 2021
Jan 8, 2025
Jul 26, 2024
Jul 24, 2024
May 26, 2024
Jul 8, 2022
Apr 1, 2023
Sep 19, 2024
Sep 19, 2024
Jul 24, 2024
Jul 26, 2024
Mar 20, 2024
Jan 8, 2025
Jul 24, 2024
Oct 5, 2023
Apr 2, 2019
Oct 5, 2023
Nov 29, 2017
Jun 11, 2024
Feb 27, 2020
Oct 1, 2020
Mar 14, 2024
Apr 15, 2024
Apr 25, 2022
Mar 16, 2022
Jan 13, 2017
Mar 16, 2022
Mar 16, 2022
Jan 7, 2025
Jul 18, 2022
Sep 30, 2020
Jul 27, 2024
Mar 8, 2022
Sep 30, 2020
Aug 26, 2022
Nov 10, 2022
Aug 19, 2022
Aug 24, 2022
Mar 8, 2022

Repository files navigation

Verified Software Toolchain

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.

How to install:

See here for instructions.

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, 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.