Relational Reasoning in Object-based Programs
summary
A program logic that weaves product programs expresses alignment points and asserts relational formulas, with a new linking rule that hides module invariants and preserves a coupling relation L; a frame rule for SMT makes heap framing decidable by SMT backends. A prototype implementation verifies examples including Dijkstra and MST and handles similar and dissimilar control and data structures. The proof system includes an explicit model of dynamic allocation and a soundness proof relative to an operational semantics.
AI-written summary · about
chapters (23)
- 0:00Intro
- 0:17Relations between programs
- 1:34Full specs needn't be available
- 2:53Relational properties: noninterference (NI)
- 5:01Data abstraction: change of data representation
- 7:25Why care?
- 7:53Relational properties: simulation
- 11:29Expressing simulation/equivalence as relation formulae
- 14:12Ingredients of reasoning (1)
- 18:16Aligning control-flow in syntax: Unary
- 19:14Aligning control-flow points in syntax: Relational
- 19:59Designating alignment in program syntax: Biprograms C C : represents executions of C, C'which are aligned on
- 21:38Change of data representation module Stack var top: Node
- 22:16Weaving for (C4 C4)
- 24:14Weaving for (BB)
- 26:29Coupling L
- 29:53Verification
- 30:57Recall: unary spec of push
- 31:23Relational spec (0) of push
- 33:12Relational logic
- 34:52Current work
- 37:12Some closely-related work
- 38:54Take away
related talks
30mAutomatic Inference of Relational Object Invariants
28mReasoning about Distributed Reconfigurable Systems
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
14mModeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…)
21mEmbedding Hindsight Reasoning in Separation Logic
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
14mA Hoare Logic For Symmetry Properties