Ownership Types for Verification of Programs with Pointer Arithmetic
summary
Extends Toman et al.’s refinement-plus-ownership type system to handle pointer arithmetic, proves soundness, and implements a prototype tool that verifies absence of assertion failures for C-style pointer code with no annotations. Key idea is per-index ownership functions (contiguous regions with linear boundaries) and a constraint pipeline that reduces unknown functions to numeric parameters, solves quantifiers by iterative instantiation (CEGAR-style), and discharges CHC queries with Spacer/Z3. Experiments verify several array-manipulating benchmarks (including a divide-and-sum) and report safe/unknown results.
AI-written summary · about
chapters (20)
- 0:00Ownership types introduction
- 1:03ConSORT verification tool review
- 3:59Fractional ownership types
- 5:47Extending ConSORT for pointers
- 9:35Typing pointer arithmetic example
- 12:11Type system formalization
- 13:59Typing rules for assignment
- 14:21Type inference overview
- 16:55Ownership constraints
- 18:20Refinement inference process
- 19:04Experimental results
- 20:31Array sum verification
- 21:17Comparison with methods
- 21:40Q&A session part one
- 24:20Q&A session part two
- 25:04Q&A session part three
- 26:10Q&A session part four
- 26:54Q&A session part five
- 27:14Q&A session part six
- 28:45Conclusion and future work
related talks
01h 26mA Path to Practically Safe C++
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
21mVIP: Verifying Real-World C Idioms with Integer-Pointer Casts
17mFat Pointers for Temporal Memory Safety of C
26mType-directed Program Transformation for Constant-Time Enforcement
17mFoundations for a Rust-Like Borrow Checker for C
28mDetecting Borrow and Provenance Bugs Across Unsafe Rust [...]
01h 25mIntroduction to Verifiable Computing