A Pure Demand Operational Semantics with Applications to Program Analysis
summary
Defines an operational semantics whose entire machine state is just a call stack plus a source program point or lexical depth, with no environment or substitution and a proof of soundness and completeness against standard environment-based semantics. Direct finitization of that semantics yields an analysis that infers recurrences instead of value-widening, stitches bounded stack fragments, emits Horn constraints solved by Spacer, and has an implementation and artifacts; evaluation vs two state-of-the-art analyzers is mixed—often tighter bounds and faster, sometimes much slower.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:21Operational semantics approaches
- 1:25Pure demand semantics
- 3:10Grammar and closures
- 4:14Function evaluation rules
- 5:17Function application example
- 7:24Correctness proof
- 7:46Semantics for program analysis
- 8:50Recursive sum stitching
- 12:20Evaluation vs analyzers
- 13:03Conclusions
- 13:46Q&A
related talks
15mSemantics of Sets of Programs
15mStable Relations and Abstract Interpretation of Higher-Order Programs
40mFormal semantics for multi-language programs- 40mFormal semantics for multi-language programs
24mTowards a Higher-Order Mathematical Operational Semantics
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
18mThe Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo...
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis