Date Added: Aug 2010
The Safety Critical Java Specification intends to support the development of programs that must be certified. The specification includes a number of annotations used to constrain the behavior of programs written against it. This paper describes and motivates the design of these annotations and the rules used to check statically that programs respect their intended semantics. The authors report on a prototype implementation with the Java Checker Framework and initial experiments annotating a 24KLoc application.