I expect this might be (or even probably is) a bad place to ask this but at the same time I didn’t find any better coming from the Contact Information page (http://sel4.systems/contact/).

I’m working on a conference paper (not sure if I will make it but still trying to – code::dive if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper – more like an update on what is the current state of the field. Yet I wanted to supply also some examples.

As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough – for this task no need to verify binary in any form.

As a side example I would like to show how your proves look like. I’m not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience “feel the size”.

If – as I expect – this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them?

Adam Badura