Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
summary
Claims a formal semantics for optimistic verification by defining gradual exact logic as a consistent lifting of exact triples over a collecting semantics, showing Hoare (overapprox) and incorrectness (underapprox) logics arise by making post or pre partial, and proving any gradual verification triple decomposes into underapproximating deductions (incorrectness-style) followed by overapproximating checks (Hoare-style). Results are theoretical for a restrictive program class, reuse ideas from gradual typing, and aim to guide future tool extensions rather than deliver a full implementation.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:25Gradual verification
- 2:10Optimistic verification example
- 3:37Incorrectness logic basics
- 5:19Motivation for connection
- 6:46Semantic definitions
- 8:53Gradual formulas and lifting
- 10:17Gradual verification as logic
- 11:00Gradual exact logic framework
- 12:22Decomposing optimistic verification
- 14:11Future work
- 14:55Summary
- 15:17Q&A
related talks
16mA Hoare-Logic Style Refinement Types Formalisation
25mA Logic for the Imprecision of Abstract Interpretations
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
30mRelatively Complete Verification of Probabilistic Programs
20mA Taxonomy of Hoare-Like Logics
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)