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

Son Ho, Aymeric Fromherz, Jonathan Protzenko

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-sca…