This paper presents a
case study of using deductive formal verification of a navigation
system from the avionics domain.  Both writing the specifications and
their verification with a runtime assertion checker and KeY, a tool
using automatic theorem proving techniques for verifying Java
programs, are covered.