Approximate Reachability for Dead Code Elimination in Esterel

Esterel is an imperative synchronous programming language for the design of reactive systems. Esterel extends Esterel with a noninstantaneous jump instruction (compatible with concurrency, preemption, etc.) so as to enable powerful source-to-source program transformations, amenable to formal verification. In this work, we propose an approximate reachability algorithm for Esterel and use its output to remove dead code. We prove the correctness of our techniques.

• Type: Conference
• Year: 2005
• Where: ATVA
• Authors: Olivier Tardieu, Stephen A. Edwards
• Keywords: ATVA 2005, Enable Powerful Source-to-source, Esterel, Imperative Synchronous Programming