A CDC (cycle double cover) of a graph G is a system (C1,...,Ck) of cycles in G such that each edge of G is contained in Ci for exactly two indices i (here a cycle is a subgraph in which each vertex has an even degree). The well-known CDC conjecture states that each bridgeless graph G has a CDC. In 1985, Goddyn proved that each minimal counterexample to the CDC conjecture has girth at least 7 (later, he even obtained the lower bound 10) by showing that each circuit C of length less than 7 is reducible, i.e. if G is a graph containing C and if G′ is obtained from G by replacing C by a certain smaller subgraph, then each CDC of G′ yields a CDC of G. Here we refine Goddyn's ideas and we present some algorithms for verifying such reduction properties. By implementing these algorithms on a computer, we can prove so far that each minimal counterexample of the CDC conjecture has girth at least 12 and we can show that each minimal counterexample of the 5-CDC conjecture (each bridgeless graph has a CDC consisting of only 5 cycles) has girth at least 10. Moreover, by using a recent result of Robertson et al. (preprint), we can prove without a computer that each bridgeless cubic graph not containing the Petersen graph as a minor has a 5-CDC which can be constructed in polynomial time. This partially settles a problem of Alspach et al..
