Verifiable C is a program logic for the C programming language:
foundational higher-order impredicative concurrent separation logic, proved sound with respect to the operational semantics of CompCert C

Books and documentation

Program Logics for Certified Compilers PLCC excerpt to chapter 3 Verifable C
(e-book)  (Kindle) (hardcover)
(free from author's page) 		Up to Chapter 3 Free download

Software downloads

Verifiable C is a component of the Verified Software Toolchain