The author first introduces foundations like C0 subset of C language and Hoare logic. Then, author then builds a library for doubly-linked lists over arbitrary data types and a string library with 11 functions which includes most-used functions.
Note: I changed tittle to say C0 instead of C to ensure accuracy. C0 is a restricted, subset of C designed to make verification easier. Author should’ve said they verified C0 code, not arbitrary C, to avoid misleading audience about method’s capabilities.