Volume 5: Verifiable C
Table of Contents
Index
Preface
Welcome
Practicalities
System Requirements
Downloading the Coq Files
Installation
Exercises
Recommended Citation Format
For Instructors and Contributors
Thanks
Check for the right version of VST
Introduction to Verifiable C (
Verif_sumarray
)
Verified Software Toolchain
How to use this textbook
A C program to add up an array
Workflow
Let's verify!
API spec for the sumarray.c program
Packaging the Gprog and Vprog
Proof of the sumarray program
Global variables and main()
Tying all the functions together
Additional recommended reading
Linked lists in Verifiable C (
Verif_reverse
)
Running Example
Inductive definition of linked lists
Hint databases for spatial operators
Specification of the
reverse
function.
Proof of the
reverse
function
The loop invariant
Why separation logic?
Stack ADT implemented by linked lists (
Verif_stack
)
Let's verify!
Malloc and free
Specification of linked lists
Specification of stack data structure
Function specifications for the stack operations
Proofs of the function bodies
A client of the stack functions (
Verif_triang
)
Proofs with integers
Specification of the stack-client functions
Proofs of the stack-client function-bodies
List segments (
Verif_append1
)
Specification of the
append
function.
List segments.
Proof of the
append
function
Additional exercises: more proofs about list segments
Additional exercises: loop-free list segments
Magic wand, partial data structure (
Verif_append2
)
Separating Implication
List segments by magic wand
Proof of the
append
function by
wlseg
The general idea: magic wand as frame
Case study: list segments for linked list box
Comparison and connection:
lseg
vs.
wlseg
String functions (
Verif_strlib
)
Standard boilerplate
Representation of null-terminated strings.
Reasoning about the contents of C strings
Function specs
A digression about size_t
Proof of the
strlen
function
Proof of the
strcpy
function
data_at is not injective!
Functional model of hash tables (
Hashfun
)
A functional model
Functional model satisfies the high-level specification
Correctness proof of hash.c (
Verif_hash
)
Function specifications
Proofs of the functions
hash
,
copy_string
,
new_cell
Proof of the
new_table
function
Auxiliary lemmas about data-structure predicates
Proof of the
get
function
Proof of the
incr_list
function
field_compatible
Where does field_compatible come from?
Proof of the
incr
function
Postcript and bibliography (
Postscript
)
Looking back
Looking forward
Small examples
Modules
Input/output
Looking around
Static analyzers
Functional correctness verifiers -- functional languages
Functional correctness verifiers -- imperative languages
Functional correctness verifiers -- C
Foundational soundness
Conclusion
Bibliography (
Bib
)
Resources cited in this volume
