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 non-instantaneous 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.
- tardieu2005approximate.pdf application/pdf 222 KB Download File
Also Published In
- Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005: Proceedings