End-to-end verification of stack-space bounds for C programs
Abstract
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 and time usage still have to be verified at the machine level where interactive proofs tend to be more tedious and automation is more challenging.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 05, 2014
- Source ID
- 10.1145/2666356.2594301
Entities
People
- Jan Hoffmann
- Quentin Carbonneaux
- Tahina Ramananandro
- Zhong Shao
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- Yale University