Sound Gradual Verification with Symbolic Execution

Explore a groundbreaking 18-minute video presentation from POPL 2024 on sound gradual verification using symbolic execution techniques. Delve into the work of researchers from Brown University, Purdue University, and Carnegie Mellon University as they address the challenges of implementing and optimizing run-time checks in gradual verification. Learn how this approach combines static and dynamic checks to support partial specifications, making verification more incremental and providing earlier feedback to developers. Discover the formalization of symbolic execution, optimized run-time check generation, and run-time execution, along with a soundness proof that extends to a core subset of the Viper tool. Gain insights into how this research uncovered and resolved a soundness bug in an implemented gradual verification tool, advancing the field of practical gradual verification.