End-to-end verification of stack-space bounds for C programs

Verified compilers guarantee the preservation of semantic properties and thus enable formal verification of programs at the source level. However, important quantitative properties such as memory a...