For all the literatures I have seen, modular reasoning for object-oriented programs is only concerned on the source code level. I'm wondering is this because we don't need modularity at low-level code, or compared to other verification challenges of bytecode, modular reasoning is, to some extent, to ...