Joachim Breitner has recently formalized Shivers' kCFA algorithm and proof of correctness in Isabelle: http://afp.sourceforge.net/entries/Shivers-CFA.shtml A Haskell prototype of the Isabelle formalization is also available on Hackage in the 'shivers-cfg' package: http://hackage.haskell.org/package/shivers-cfg David