Gradual verification supports partial specifications by soundly applying static checking where possible and dynamic checking when necessary. This approach supports incrementality and provides a formal guarantee of verifiability. The first gradual verifier, Gradual $C_0$, supports programs that manipulate recursive, mutable data structures on the heap and minimizes dynamic checks with statically available information. The design of Gradual $C_0$ has been formally proven sound; however, this guarantee does not hold for its implementation.

In this paper, we introduce a lightweight approach to testing soundness of Gradual $C_0$’s implementation. This approach uses Property Based Testing to empirically evaluate soundness by establishing a truthiness property of equivalence. Our approach verifies a test suite of incorrectly written programs and specifications with both Gradual $C_0$ and a fully dynamic verifier for $C_0$, and then asserts an equivalence between the results of the two verifiers using the dynamic verifier as ground truth. Any inconsistency between the results, indicates a problem in Gradual $C_0$’s implementation. We also show in this paper, as a proof of concept, that this lightweight approach to testing Gradual $C_0$’s soundness caught a number of significant implementation bugs from Gradual $C_0$’s issue tracker in GitHub. A number of these bugs were only previously caught by human inspections of internal output of the tool. An automated generator for the test suite is our next research step to increase the rigor of our evaluation and catch new bugs never found before.

I’m an undergrad @ Cornell University working towards computer science and philosophy degrees. My main research goals involve developing practical tools for software verification in general and domain-specific cases through programming language theory.