Semantic Transformation Framework for Rewriting Rules
summary
Refines Cousot & Cousot by tailoring a semantic transformation framework to rewriting rules and builds a four-part pipeline: matcher/meter, syntactic substituter, semantic substituter and a correctness argument split into base and inductive cases. Uses trace semantics plus static analyses (value analysis, liveness) and proves semantics preservation for six concrete transformations (constant propagation, dead-assignment elimination, etc.). Introduces theorems like concatenation preservation and final-state preservation to discharge most inductive proofs, and completes manual base-case proofs so the framework verifies those six examples.
AI-written summary · about
chapters (15)
- 0:00Start
- 1:38Issues in Rewriting-rule based Program Transformation
- 5:19Issues in Semantic Transformation Framework
- 6:49Target Transformations
- 7:30Target Language
- 7:47Concrete Semantics
- 9:08High-level Overview of Our Approach
- 9:36Matcher for Constant Propagation
- 10:55Syntactic Substituter for Constant Propagation
- 11:42Semantic Substituter for Constant Propagation
- 13:38Correctness Argument - Base Case
- 15:03Correctness Argument - Inductive Case
- 17:55Properties of Semantic Substituter
- 18:34Exploiting the Properties of Transformation
- 19:10Defining Example Transformations
related talks
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
25mA Semantic Approach to Robust Property Preservation
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
21mSynthesizing Formal Semantics from Executable Interpreters
15mSulfur: Substitution Generation using a Logical Framework
15mA Semantic Framework for PEGs
27mAugmenting Rewrite Rule Sets via Knuth-Bendix Completion
01h 05mAll the Languages Together