Symbolic Execution for Randomized Programs
summary
Adds probabilistic symbolic variables to symbolic execution and computes symbolic probability expressions for paths, then checks universal quantitative properties by sending SMT queries to Z3. Implements the technique as Plinko (KLEE) on LLVM bitcode and verifies randomized C++ case studies (Freivalds’ algorithm, randomized quicksort, reservoir sampling, monotonicity testing); most benchmarks finish within ten minutes and one case reveals a bug in a Bloom filter. Empirical comparisons show 55x faster than PSI after algebraic simplifications and verifies over all 32-bit integers in 75s where STORM times out.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:25Motivation: Paper Approach
- 3:26Motivation: Monty Hall-as-code
- 5:37Handling Random Sampling Statements
- 8:15Three System Components
- 9:07Key Idea 1: Probabilistic Symbolic Variables
- 11:02Key Idea 2: Computing Branch Probabilities
- 13:06Key Idea 2: Branch Probabilities
- 16:10Key Idea: SMT Query
- 18:37Implementation: PLINKO
- 19:31Evaluation: Questions
- 23:44Reservoir Sampling
- 24:02Comparison: Storm
- 25:42Sumit Lahiri Symbolic Execution for Subhajit Roy Randomized Programs
related talks
20mDerivative-Guided Symbolic Execution
01h 01mSymbolic Execution in .NET
42mSurprise yourself with Property Based Testing
20mSemantic Reification: A New Paradigm for Random Program Generation
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
15mTuning Random Generators: Property-Based Testing as Probabilistic Programming
47mQuickSpec: A Lightweight Theory Exploration Tool (...)
30mLet's Build a Symbolic Analyser And Automatically Find Bugs