Formal Methods to Save the Earth
summary
Computes a deductive program logic called Power Logic with small-step operational semantics that separate instantaneous vs lasting energy and model a footprint like separation logic; proves two theorems showing a program uses identical energy from two states when it leaves power state unchanged and the states agree on the program’s footprint; stays symbolic (instruction energy = α) so values plug in per platform; delivers formal rules and frame reasoning but no full proof assistant yet, and caches/pipelines and physical soundness remain open.
AI-written summary · about
chapters (7)
- 0:00Formal methods for energy efficiency
- 3:13Energy efficiency limitations
- 7:02Power logic for energy reasoning
- 10:13Power and data states framework
- 12:25Theorems in power logic
- 14:15Power logic strengths and limits
- 15:40Conclusion
related talks
52mThink Abstractly, Work Concretely
34mLogic in Computer Science, Engineering and Industry
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
19mPete's Footprints
40mFormal semantics for multi-language programs
46mKeynote: Formal Verification? No, Formal Reasoning!
23mSpecifying and Verifying Future Conditions
22mExecution Time Program Verification With Tight Bounds