Within the research surrounding the verification and inference of program
invariants our chair developed a framework
to generate control flow graphs from Java source code. Within this framework,
a developer can implement analyses based on fixpoint computations. Our
Analyzer tool is capable of visualisation and animation of such fixpoint
algorithms, providing a useful interface for the surveillance of such
algorithms. Researchers can implement their own analyses by overriding one of
our fixpoint iteration classes, thus rapidly developing a nicely displayable
program analysis without the flaw of fussing around with graphics too much.