Visual DbC

Visual DbC is a proof management and visualization tool. It allows to visualize code members (e.g. types, attributes, methods) together with specifications (e.g. method contracts, invariants) and proofs in a DbC diagram similar to an UML class diagram. Proof references are used to indicate that a code member or a specification is used by a proof.

The following sections illustrate the main features of Visual DbC using screenshots. Each section contains numbered screenshots that explain a usage scenario step by step. Clicking on each picture produces a more detailed view. The screenshots may differ from the latest release.


Visual DbC is compatible with Eclipse Indigo (3.7) or newer.

Required update-sites and installation instructions are available in the download area.

Visualize existing source code

Do proofs with a DbC diagram

Visualize proof dependencies of a proof in the KeYIDE

KeY basics in Eclipse and troubleshooting