Hi everyone, We are developing a bounded model checker for C/C++ called CBMC here at the University of Oxford. We're currently evaluating different options to implement a Java frontend for the program, allowing us to statically verify Java code as well.
There's obviously a whole series of problems to be tackled before this is possible, one of which is the following: In order to provide a reasonable scope, the verifier needs to know the semantics of native JRE library code. One way of allowing us to do so is for our program to model JNI and use OpenJDK's C/C++ implementations to determine the semantics of such a method call in Java. This approach begs the following questions: 1.) Are all native runtime library operations in OpenJDK implemented in proper JNI or are there exceptions and caveats to this approach? 2.) Are the implementations of these functions reasonably detached from each other and the rest of the VM, such that they can be analysed in isolation? Thanks for a quick heads-up on this and best, Pascal
