Claude Bolduc, Béchir Ktari: Visibly Pushdown Kleene Algebra and Its Use in Interprocedural Analysis of (Mutually) Recursive Programs. RelMiCS 2009: 44-58