Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910722223505408 |
|---|---|
| author | Zimmerman, Conrad DiVincenzo, Jenna |
| author_facet | Zimmerman, Conrad DiVincenzo, Jenna |
| contents | Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing [Garcia et al. 2016]. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_00339 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification Zimmerman, Conrad DiVincenzo, Jenna Logic in Computer Science Programming Languages Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing [Garcia et al. 2016]. |
| title | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2412.00339 |