Abstract
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.
References
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.
https://doi.org/10.1145/357766.351266
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
(2022).
Eilers, M. & Müller, P. (2018). Nagini: a static verifier for Python. In International Conference
on Computer Aided Verification. Springer, 596–603.
https://doi.org/10.1007/978-3-319-96145-3_33
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.
https://doi.org/10.3929/ethz-a-010835519
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.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Copyright (c) 2023 Jan-Paul Ramos