Gradual C0: Symbolic Execution for Gradual Verification

Static verification tools for heap-manipulating programs, such as those based on separation logic, typically require complete, detailed specifications. This creates a significant burden on users, who must provide complex auxiliary specifications like loop invariants and inductive lemmas before receiving any feedback on their code. Gradual C0 addresses this by implementing a gradual verification system for C0, a safe subset of C. It allows developers to write partial or missing specifications, which are then soundly checked through a combination of static symbolic execution and dynamic run-time monitoring.

Gradual C0 extends the Viper verification infrastructure by integrating symbolic execution with imprecise specifications. Unlike previous gradual verification proposals that relied on weakest liberal preconditions, Gradual C0 uses symbolic execution to track heap ownership and functional properties. When specifications are imprecise, the verifier makes optimistic assumptions and automatically generates minimized run-time checks. These checks are encoded directly into the C0 source code, allowing the program to be compiled and executed with dynamic verification. The system tracks heap ownership dynamically using a hash table, ensuring that memory safety and functional properties are maintained even when static proofs are incomplete.

Empirical evaluation across four data structures (BST, Linked List, Composite Tree, and AVL Tree) demonstrates that Gradual C0 successfully balances static and dynamic verification. As developers add more precise specifications, the system statically discharges more proof obligations, leading to a measurable reduction in run-time overhead compared to fully dynamic approaches. The study reveals that while increasing precision generally improves performance, there are specific thresholds where the cost of dynamic ownership tracking can temporarily increase overhead. The authors provide actionable strategies for developers, such as specifying frequently executed code in fully verifiable chunks to minimize the performance impact of dynamic boundary checks.