Verification and inference of program invariants

Verification and inference of program invariants: CFG Analysator

Related people:

System:

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.

Screenshot

Analysis projects:

System requirements

Sourcecode

The sourcecode for our framework is freely available in our SVN under the GPL.

Related Publications: