Think Abstractly, Work Concretely
summary
Uses while dt programs that replace continuous flows by infinitesimal jumps and gives a semantics via hyperreals and an ultrafilter so formulas satisfy the transfer principle; defines section-wise execution by expanding hyperreals into sequences, proving soundness and relative completeness of a Hoare-style logic and enabling invariant generation and abstract interpretation to target hybrid systems; clarifies that the language is a modeling (not executable) device, and argues logic can still strengthen black‑box testing and guide model‑free verification of CPS.
AI-written summary · about
chapters (8)
- 0:00Introduction and context
- 5:02Non-standard analysis
- 9:20Mathematical foundations
- 17:26Logic and semantics
- 26:09Research lessons and CPS
- 32:18Model-free verification
- 36:50Collaboration and tips
- 42:00Q&A and concluding remarks
related talks
01h 05mVerifying Infinitely Many Programs at Once
28mReasoning about Distributed Reconfigurable Systems
36mThe Abstract Method, In General
27mUnrealizability Logic
34mLogic in Computer Science, Engineering and Industry
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)