Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
summary
Dynaplex instruments recursive programs, infers recurrences from traces (sizes, recursion depth, loop counts), fits cost terms by regression, and solves with master theorem and pattern matching to produce closed‑form Big O bounds. It reports O(n log n) for mergesort, 2^n for Tower of Hanoi, and n^1.58 for Karatsuba, and it evaluates on 37 programs across Python/C/OCaml, producing correct complexity for 32/37 (two cases had wrong recurrences but right bounds, three were incorrect). Plans include fuzzing for worst‑case traces and static verification.
AI-written summary · about
chapters (6)
- 0:00Start
- 2:01Overview of Dynaplex's Architecture
- 3:20Recursive Implementation of Merge Sort
- 7:59Dynaplex Compute the Complexity of Fibonacci Sequence
- 8:10Fibonacci Sequence
- 8:38Fibonacci Program
related talks
51mAlgorithms Demystified
13mDynamiTe: Dynamic Termination and Non-termination Proofs
47mComplexity is a Sin
22mExecution Time Program Verification With Tight Bounds
36mStatic Analysis of APL for Tooling and Compliance
24mPolynomial-Time Program Equivalence for Machine Knitting
13mMetamorph: Synthesizing Large Objects from Dafny Specifications
26mTowards Efficient Model Comparison Using Automated Program Rewriting