Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE(…)
summary
Phocus synthesizes sound, precise abstract transformers for Lax‑Friedrichs, Leapfrog and Upwind finite difference schemes by finding a best linear approximation and solving a nonconvex optimization to compute a tight sound enclosure D. It certifies numeric invariants such as the CFL condition, bounds total variation and the absence of shock formation, and outperforms naive zonotope composition on Burgers benchmarks. Evaluation reports tight bounds and scalability to over 5,000 mesh points across hundreds of time steps.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:03Hyperbolic PDEs significance
- 2:32Numerical methods for PDEs
- 3:38Finite difference schemes
- 4:43FOCUS tool core idea
- 6:10Continuous optimization for bounds
- 7:14PDE properties verification
- 8:59Benchmark results
- 11:03Tool capabilities
- 11:26Q&A
related talks
22mSAIL: Sound Abstract Interpreters with LLMs
28mSynthesizing Abstract Transformers
20mOptimal Program Synthesis via Abstract Interpretation
14mHigher-order Automation In TLAPS
18mMobius: Synthesizing Relational Queries with Recursive and Invented Predicates
01h 05mFrom meta frameworks and transformations to distributed computing and more
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
01h 10mThe Rise & Collapse of a Quantum State