Inference of Resource Management Specifications
summary
Automatic inference produces resource-management specs for Java and C# by applying optimistic inference rules framed in a Datalog-style fixpoint so the system infers who owns and must close resources even when code has bugs. Implementations integrate with the Checker Framework and a CodeQL/C# pipeline. Evaluation over benchmarks recovers about 85.5% of manually written annotations, yields nearly the same verifier false-alarm rate as hand annotations, and surfaces new real bugs.
AI-written summary · about
chapters (8)
- 0:00Resource management spec inference
- 1:03Resource leak detection approach
- 3:12Motivation for annotation inference
- 8:07Key challenges in inference
- 9:55Optimistic inference approach
- 12:44Experimental results
- 15:33Summary and future work
- 16:18Q&A
related talks
15mData-Driven Abductive Inference of Library Specifications
23mSpecifying and Verifying Future Conditions
30mAutomatic Inference of Relational Object Invariants
20mAutomatic and Incremental Repair for Speculative Information Leaks
13mRevealing Sources of (Memory) Errors via Backward Analysis
28mGradual Verification: Assuring Software Incrementally
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
22mFormal Runtime Error Detection During Development in the Automotive Industry