Skip to Main content Skip to Navigation
Conference papers

Fast Computation of Arbitrary Control Dependencies

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Delphine Le Piolet <>
Submitted on : Friday, April 10, 2020 - 10:48:55 AM
Last modification on : Thursday, July 2, 2020 - 9:12:02 AM

Links full text



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⟩



Record views