Fast Computation of Arbitrary Control Dependencies - CentraleSupélec Access content directly
Conference Papers Year : 2018

Fast Computation of Arbitrary Control Dependencies


In 2011, Danicic et al. introduced an elegant generalization of the notion of control dependence for any directed graph. They also proposed an algorithm computing the weak control-closure of a subset of graph vertices and performed a paper-and-pencil proof of its correctness. We have performed its proof in the Coq proof assistant. This paper also presents a novel, more efficient algorithm to compute weak control-closure taking benefit of intermediate propagation results of previous iterations in order to accelerate the following ones. This optimization makes the design and proof of the algorithm more complex and requires subtle loop invariants. The new algorithm has been formalized and mechanically proven in the Why3 verification tool. Experiments on arbitrary generated graphs with up to thousands of vertices demonstrate that the proposed algorithm remains practical for real-life programs and significantly outperforms Danicic’s initial technique.

Dates and versions

hal-02539534 , version 1 (10-04-2020)



Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall. Fast Computation of Arbitrary Control Dependencies. FASE 2018 International Conference on Fundamental Approaches to Software Engineering, Apr 2018, Thessaloniki, Greece. pp.207-224, ⟨10.1007/978-3-319-89363-1_12⟩. ⟨hal-02539534⟩
50 View
0 Download



Gmail Facebook Twitter LinkedIn More