calling context In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling conte

calling context In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling context. spec very similar to this Yes, I was using something similar. Note that this is right only in a purely sequential setting ... I recently verified a JIT compiler, That sounds exciting. That must have been a major piece of work. Anything published yet? With JIT compilers the issue of self-modification becomes pertinent. I know that Magnus Myreen has verified a small JIT compiler a few years back but I don't remember exactly what theorem he proves. IIRC he was using a tailor-made Hoare logic for x86 code that basically moved some of the complexity of the spec into the logic.