Program Analysis via Efficient Symbolic Abstraction
summary
Two algorithms compute most-precise abstractions for quantifier-free bit-vector formulas over the interval and a convex polyhedral-like domain, using SMT/OMT-guided search that samples extreme models and interleaves arbitrary-model and interval-based sampling. Implementations target static memory-corruption analysis and constrained random fuzzing, evaluated on 57,933 queries, and achieve 2.1 to 17.6× speedup versus prior OMT/MaxSAT encodings while solving dozens to hundreds more queries (e.g., +12–320 and +188 on average).
AI-written summary · about
chapters (25)
- 0:00Intro
- 0:15Abstract Interpretation
- 0:35Best (Most Precise) Abstract Transformer
- 1:14Specification of Best Abstract Transformer
- 2:07Symbolic Abstraction in Logical Form
- 2:53Why Using Symbolic Abstraction
- 3:42Key Observation and Idea
- 4:34Example of Symbolic Interval Abstraction
- 4:46OMT-based Symbolic Interval Abstraction
- 5:07SMT-based, Binary-Search-Style OMT Solving
- 5:45Problem: Handing Many Objective Functions
- 6:00Solution: Utilize Correlations of the Objectives
- 6:58Key Idea Behind RSY's Algorithm
- 7:38Example of Symbolic Polyhedral Abstraction
- 7:56Naïve Solution for Symbolic Polyhedral Abstraction
- 8:09RSY for Polyhedral Abstraction
- 8:51Problem: The "Arbitrary" Models May Not Generalize Well
- 9:21How Do Extremal Models Help
- 9:49Challenge: How to Compute the Extremal Models
- 10:01Solution: Abstraction from Symbolic Interval Abstraction
- 10:39The Rest of the Story...
- 11:11Evaluation
- 11:24Queries from the Benchmarks
- 12:25Summary
- 12:51Related Problems
related talks
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
20mOptimal Program Synthesis via Abstract Interpretation
30mAnalyzing Programs with SMT Solvers
18mScalable Floating-Point Satisfiability via Staged Optimization
46mMechanizing Abstract Interpretation
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
13mOn the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)