Son Ho

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

2021 · arXiv (Cornell University)

For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments. We present the design, implementation and evaluation of …