Quantified Underapproximation via Labeled Bunches
summary
Presents a formal system that lets over‑ and under‑approximate analyses compose soundly by attaching a test-level modality that ranges over component internal resource values (example: OBC/IRS reuse and Ariane 5 failure). Builds a sequent calculus LabelBI on bunched implications, gives trace semantics, and proves soundness and cut elimination. Implements an OCaml implementation that performs proof search (nonterminating so it accepts user hints); artifacts and reproducible results are published.
AI-written summary · about
chapters (10)
- 0:00Quantified underapproximation intro
- 1:04Composing testing analyses
- 2:28Ariane 5 failure formalization
- 4:40Test levels in components
- 7:30Unifying interpretations with bunching
- 8:56Extending BI logic with tests
- 10:23Kripke semantics for judgments
- 11:27Label BI calculus
- 12:30Related work and future
- 13:16Q&A
related talks
20mOn Extending Incorrectness Logic with Backwards Reasoning
23mSpecifying and Verifying Future Conditions
15mData-Driven Abductive Inference of Library Specifications
22mExecution Time Program Verification With Tight Bounds
22mA Categorical Basis for Robust Program Analysis
52mThink Abstractly, Work Concretely
24mBuilding Information Modeling Using Constraint Logic Programming (Extended Ab...
26mUnification for Subformula Linking under Quantifiers