A Pointer-Ownership Model for C Inspired by Rust
summary
An end-to-end system builds per-function P models (ownership + lifetimes), uses an LLM-assisted builder to fill models, and checks them with a SAT solver that returns unsat cores. Implementation analyzes 4,604 Juliet C examples for five temporal-CWE classes, flagging all memory-unsafe cases and classifying 81% of the 2,302 safe examples as safe. On a real utility (dos2unix) the LLM labels 159 of 169 pointers correctly (94.1%); hallucinations produce unsat cores rather than false negatives.
AI-written summary · about
chapters (10)
- 0:00Pointer ownership in C
- 1:49Formal methods beyond academia
- 4:01Pointer ownership examples
- 6:11Building P model
- 8:19Testing with real-world code
- 11:30Juliet test results
- 15:01LLM builder and SAT solver
- 16:31Future work
- 17:56Conclusion
- 18:38Q&A
related talks
20mData-oriented Design for Differentiable, Probabilistic Programming
19mProgrammable MCMC with Soundly Composed Guide Programs
49mIntroduction to Linear Type Systems and Linear Haskell
15mAyudante: A Deep Reinforcement Learning Approach to Assist Persistent Memory...
18mConcrete Type Inference for Code Optimization using Machine Learning with SMT S...
15mLearning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Featu
06mLightning Talk: Curry-Howard Correspondence
44mDown the Wabbit Hole