Semantics of Sets of Programs
summary
Claims that compositional verification of simple properties for infinite program sets with loops requires tracking behaviors across unbounded executions, and proves necessity and sufficiency. Builds a denotational multi-execution semantics that interprets programs as functions on power sets of lists of states, proves it is the minimal compositional extension of the single-execution semantics, and derives a sound, relatively complete Hoare-style logic for sets of programs that handles loops.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 2:07Defining semantics for sets
- 4:54Single execution fails for loops
- 7:00Non-compositionality in loops
- 10:52Multi-execution semantics for loops
- 12:57Properties and minimal extension
- 13:41Q&A
related talks
17mDenotation-based Compositional Compiler Verification
19mA Pure Demand Operational Semantics with Applications to Program Analysis
40mFormal semantics for multi-language programs
22mCategorical Semantics of Probabilistic Symbolic Execution- 40mFormal semantics for multi-language programs
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
15mStable Relations and Abstract Interpretation of Higher-Order Programs
30mRelatively Complete Verification of Probabilistic Programs