| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A Fast Verified Liveness Analysis in SSA Form
Abstract : Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. [7] designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert's benchmarks with respect to the classic data-flow-based liveness analysis, and observe performance gains.
Cited literature [18 references]
https://hal.inria.fr/hal-02904204
Contributor : Sandrine Blazy <>
Submitted on : Tuesday, July 21, 2020 - 6:05:21 PM
Last modification on : Thursday, January 7, 2021 - 4:13:40 PM
Long-term archiving on: : Tuesday, December 1, 2020 - 3:58:01 AM
Contributor : Sandrine Blazy <>
Submitted on : Tuesday, July 21, 2020 - 6:05:21 PM
Last modification on : Thursday, January 7, 2021 - 4:13:40 PM
Long-term archiving on: : Tuesday, December 1, 2020 - 3:58:01 AM
File
ijcar20_final.pdf
Files produced by the author(s)