Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11562948_25 | ATVA |
Keywords | DocType | Volume |
non-instantaneous jump instruction,approximate reachability algorithm,reactive system,imperative synchronous programming language,dead code,dead code elimination,powerful source-to-source program transformation,formal verification | Conference | 3707 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-29209-8 | 1 |
PageRank | References | Authors |
0.35 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olivier Tardieu | 1 | 462 | 32.13 |
| Stephen A. Edwards | 2 | 1443 | 109.65 |