Arbitrary control dependence

This site presents a formalization in the Coq proof assistant of a theory about weak control dependence (Danicic et al., 2011). It also contains a Why3 formalization of an algorithm computing weak control-closure optimizing Danicic's algorithm, along with OCaml manual implementations of both algorithms for performance comparisons.

This work is also detailed in the associated publications. The archive is available here.