Verifiable C: Applying the Verified Software Toolchain to C programs (also included in doc/ directory of VST distribution).
Software Foundations Volume 5: Verifiable C, by Andrew W. Appel and Qinxiang Cao, 2020.
Program Logics for Certified Compilers, by Andrew W. Appel et al.,
Cambridge University Press, 2014.
E-book; Hardback from publisher; Hardback from Amazon.com
VST relies on CompCert for some purposes. The CompCert license permits some parts of CompCert to all users, and other parts only to licensed users. Whether or not you are a licensed user, you may use VST; but only licensed users may process .c files through CompCert's clightgen tool (among other things).
You are a licensed user if your use "relates only to educational, research, personal or evaluation purposes" or if you have purchased a license from AbsInt.com.
If you are licensed user, you may use full CompCert,
opam install coq-compcert.3.7+8.12~coq_platform
If you are not a licensed user, you may use
only the open-source portions of CompCert.
Before installing coq-vst, install CompCert by:
opam install coq-compcert.3.7+8.12~coq_platform~open_source