Automatic Inference of Relational Object Invariants
summary
Claims an Abstract Interpretation method that infers relational object invariants by splitting memory into banks and keeping a most-recently-used cache entry for strong updates so temporary invariant breaks do not destroy summaries. Implements a reduced product domain mixing numerical (e.g., octagons) and equality subdomains, ships it in the CRAB abstract interpreter, and evaluates on memory-safety benchmarks and as a pre-pass to SEABMC. Results show better scalability than prior CRAB and that many assertions are discharged and SEABMC runtimes improve.
AI-written summary · about
chapters (17)
- 0:00Relational object invariants
- 1:04Inferring memory object properties
- 3:29Allocation site abstraction
- 5:15Recency abstraction limits
- 6:59Recent use abstraction
- 8:25Concrete semantics for domains
- 11:14Memory model with cache
- 15:28Abstract domain design
- 17:32Abstract execution walkthrough
- 20:23Invariants after loops
- 21:07Q&A on cache utility
- 22:34Q&A on object count domains
- 23:59Q&A on equality domain
- 24:42Experimental validation
- 26:48Integration with model checking
- 27:53Q&A on complex invariants
- 28:56Q&A on quantified invariants
related talks
40mRelational Reasoning in Object-based Programs
30mUnconstrained Variable Oracles for Faster Static Analyses
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
18mInference of Resource Management Specifications
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
15mThread-modular Analysis of Release-Acquire Concurrency