From Batch to Stream: Automatic Generation of Online Algorithms
summary
Automated method extracts a relational function signature via static analysis, builds initial state by evaluating each spec on the empty list, and synthesizes update code by decomposing sketches and combining symbolic reasoning with search. Implemented as Opera, it converts batch folds into streaming updaters, handling nonlinear cases like Welford’s variance. Evaluation on 52 benchmarks across statistics and auctions yields 98% success (50/51 synthesized within ~25s), outperforming CVC5 and Sketch, artifacts available.
AI-written summary · about
chapters (6)
- 0:00Online vs offline algorithms
- 3:26Problem statement and equivalence
- 7:25Relational specification and analysis
- 10:18Deductive synthesis and equivalence
- 13:29Evaluation and results
- 15:34Q&A
related talks
22mProgram Synthesis for Artifacts beyond Programs
19mConcurrent Data Structures Made Easy
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
15mAutomatic Synthesis of Data-Flow Analyzers
01h 06mDesigning Applications with Functional Programming Constructs
41mConcurrent Stream Processing
13mMetamorph: Synthesizing Large Objects from Dafny Specifications
52mThink Abstractly, Work Concretely