Integrating Tools for Automatic Program Verification

Abstract. In this paper we describe our findings after integrating sev-eral tools based upon the Java Modeling Language (JML) [1], a specifi-cation language used to annotate Java programs. The tools we consider are Daikon [2], ESC/Java [3], JML runtime assertion checker [1], and Loop/PVS tool [4]. The first one generates specifications; the others are used to verify them. We find that for the first three it is worthwhile to combine them because this is relatively easy and it improves the spec-ifications. Combining Daikon and the Loop/PVS tool directly works in theory, but in practice it only works if the test suite is very good and hence it is not advisable.