A case study of specification and verification using JML in an avionics application
Peter H. Schmitt, Isabel Tonin, Claus Wonnemann, Éric Jenn, Stéphane Leriche, James J. Hunt · 2006
The literature for deductive formal verification is quite rich; however, very few case studies have been done. The authors present 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.