Jacob Gorenburg

Gradual C0: Symbolic Execution for Gradual Verification

2024 · ACM Transactions on Programming Languages and Systems

Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior …