Automatically Deriving Control-Flow Graph Generators from Operational Semantics
summary
An algorithm converts small-step operational semantics into an abstract machine, then uses abstract rewriting to synthesize both interpreted-mode and standalone CFG generators; the implementation Mandate produces human-readable code for two languages with 60–80 rules each. The approach lets two parameters (abstraction and projection) yield many CFG variants, automatically derives a 43-node pattern for a Tiger for-loop, proves correspondence to the original semantics and provides an automated termination proof for interpreted generators.
AI-written summary · about
chapters (7)
- 0:00The need for automation
- 2:01Understanding CFGs
- 4:21Defining from principles
- 5:38The conversion algorithm
- 9:08Pattern generation
- 12:39Customizable generators
- 14:47Conclusion and future work
related talks
20mCertified Abstract Machines for Skeletal Semantics
21mSynthesizing Formal Semantics from Executable Interpreters
20mSemantic Reification: A New Paradigm for Random Program Generation
23mAn Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
24mAutomated extraction of grammar optimization rule configurations in a metamodel-gr...
30mFormal Metatheory of Second-Order Abstract Syntax
29mSemantic Transformation Framework for Rewriting Rules
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)