5 ms·
It seems very interesting, thank you. What's the relationship with the original jbmc project?
by emme 3mo ago
It seems very interesting, thank you. What's the relationship with the original jbmc project?
- Grover_c13 3mo agoWe use JBMC as the engine to do the verification (unmodified). bmc4j is independent of the group, we just use the tooling (similar to kani using cbmc). if you used you it may be aware of the gaps when it comes to java, so bmc4j does leg work to fill it in (lots of JDK modelling, kotlin intrinsics, some byte-code transformation to fill in soundness holes) while trying making the developer experience not so painful.
- emme 3mo agoYes, great work, thank you. I tried it a bit, and the experience is much more pleasant than using jbmc directly.