LARA Run-time checking We are exploring various aspects of run-time checking. Some of our work so far in the context of Separation logic run-time checker Run-time checker for Jahob Specification Compiler for Bytecodes