Academic Commons

Articles

Approximate Reachability for Dead Code Elimination in Esterel*

Tardieu, Olivier; Edwards, Stephen A.

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.

Subjects

Files

  • thumnail for tardieu2005approximate.pdf tardieu2005approximate.pdf application/pdf 222 KB Download File

Also Published In

Title
Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005: Proceedings
Publisher
Springer
DOI
https://doi.org/10.1007/11562948_25

More About This Work

Academic Units
Computer Science
Series
Lecture Notes in Computer Science, 3707
Published Here
March 8, 2012