Skip to Main content Skip to Navigation
Conference papers

A Fast Verified Liveness Analysis in SSA Form

Jean-Christophe Léchenet 1 Sandrine Blazy 1 David Pichardie 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Tuesday, July 21, 2020 - 6:05:21 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM
Long-term archiving on: : Tuesday, December 1, 2020 - 3:58:01 AM


Files produced by the author(s)



Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA Form. IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩. ⟨hal-02904204⟩



Record views


Files downloads