Vodpuk is a tool for helping Timbuk works.

Timbuk is a tree automata library which implements usual operations on tree automata as well as a completion algorithm used to prove the unreachability of the banned properties of systems which you have to verify.

Timbuk done this work by computing an over-approximation of descendants for a set of initial terms from a program. The intial terms are corresponding to all function calls and initial configurations of process which are coming from the program.

But work with Timbuk is hard when initial terms of programs bring the production of several diverging tree automata. You cannot know where and when they appear. It becomes harder to assess the over-approximations.

The first aim for "Vodpuk" is to provide the visualization of divergence points in Timbuk analysis. The second one is to generate automaticaly over-approximation equations for building a finite automaton.