[seL4] How to prove correctness of my own program?
adam.f.badura at gmail.com
Tue May 30 09:24:05 AEST 2017
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
I'm working on a conference paper (not sure if I will make it but still
trying to - code::dive <http://codedive.pl/> 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?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Devel