Using an example from avionics software we will first describe the use
 of the Java Modeling Langugae (JML). Next we will shortly introduce
 our formal verification tool, the KeY tool, and its underlying logic,
 which is a version of Dynamic Logic taylored towards verfication of
 Java programs. The JML specification are translated into the input
 language of our interactive theorem prover and proved.