Evaluating Soundness of a Gradual Verifier with Property Based Testing


software verification
computer science
property based testing

How to Cite

Ramos, J.-P. (2023). Evaluating Soundness of a Gradual Verifier with Property Based Testing. Cornell Undergraduate Research Journal, 2(1), 17–27. https://doi.org/10.37513/curj.v2i1.696


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 C0, supports programs that manipulate recursive, mutable data structures on the heap and minimizes dynamic checks with statically available information. The design of Gradual C0 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 C0'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 C0 and a fully dynamic verifier for C0, 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 C0's implementation. We also show in this paper, as a proof of concept, that this lightweight approach to testing Gradual C0's soundness caught a number of significant implementation bugs from Gradual C0'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.



Bader, J., Aldrich, J., & Tanter, É. (2018). Gradual Program Verification. In

International Conference on Verification, Model Checking, and Abstract Interpretation.

Springer, 25–46.

Astrauskas, V., Müller, P., Poli, F., & Summers, A. (2019). Leveraging Rust types for modular

specification and verification. Proceedings of the ACM on Programming Languages 3,

OOPSLA (2019), 1–30. https://doi.org/10.1145/3360573

Claessen, K., & Hughes, J. (2000). QuickCheck: A Lightweight Tool for Random Testing of

Haskell Programs. SIGPLAN Not. 35, 9 (sep 2000), 268–279.


DiVincenzo, J., McCormack, I., Gouni, H., Gorenburg, J., Zhang, M., Zimmerman, C.,

Sunshine, J., Tanter, É., & Aldrich, J. (2022). Gradual C0: Symbolic Execution for

Efficient Gradual Verification. arXiv preprint arXiv:2210.02428


Eilers, M. & Müller, P. (2018). Nagini: a static verifier for Python. In International Conference

on Computer Aided Verification. Springer, 596–603.


Garcia, R., Clark, A., & Tanter, É. (2016). Abstracting Gradual Typing. In

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of

Programming Languages (St. Petersburg, FL, USA) (POPL ’16). ACM, New York, NY,

USA, 429–442. https://doi.org/10.1145/2837614.2837670

Parkinson, M., & Bierman, G. (2005). Separation logic and abstraction. In ACM

SIGPLAN Notices, Vol. 40. ACM, 247–258.

Reynolds, J. (2002). Separation logic: A logic for shared mutable data structures. In Logic in

Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on. IEEE, 55–74.

Schwerhoff, M. (2016). Advancing Automated, Permission-Based Program Verification Using

Symbolic Execution. Ph.D. Dissertation. ETH Zurich.


Smans, J., Jacobs, B., & Piessens, F. (2009). Implicit dynamic frames: Combining dynamic

frames and separation logic. In European Conference on Object-Oriented Programming.

Springer, 148–172. https://doi.org/10.1007/978-3-642-03013-0_8

Siek, J., & Taha, W. (2007). Gradual typing for objects. In European Conference on

Object-Oriented Programming. Springer, 2–27.

Siek, J., & Taha, W. (2006). Gradual typing for functional languages. In Scheme and Functional

Programming Workshop, Vol. 6. 81–92.

Wise J., Bader J., Wong, C., Aldirch, J., Tanter, É., & Sunshine, J. (2020). Gradual verification

of recursive heap data structures

Wolf, F., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J., & Müller, P. (2021). Gobra:

Modular Specification and Verification of Go Programs. In International Conference on

Computer Aided Verification. Springer, 367–379.


Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Copyright (c) 2023 Jan-Paul Ramos