Sound Gradual Verification with Symbolic Execution
summary
Provides a formal, machine-checked semantics for symbolic execution and for optimized runtime-check generation, proves that gradual verification implemented this way is sound, and applies the proof to a core subset of Viper (first such result). Finds a concrete unsoundness in an existing gradual verifier, patches the semantics with an exclusion frame rule to prevent overlapping permissions, and shows the repaired system enforces safe execution and that all gradual specifications are actually validated at runtime.
AI-written summary · about