Design and Implementation of a Gradual Verifier
Static program verification requires a large number of user-provided specifications, resulting in a significant upfront verification cost. One method for reducing this burden is gradual verification, a novel approach that enables developers to deal with the cost of verification incrementally—statically where possible and dynamically where necessary. In this paper, we discuss our work designing and implementing the static portion of a gradual verification tool.
|Design and Implementation of a Gradual Verifier (SPLASH '20 Poster.pdf)||3.43MiB|