[SystemSafety] proofs

[Olwen Morgan]

... just cogitating out loud ... an unsavoury habit that some of us old 
windbags have acquired over the years ...

... anyway, I suggested the double-blind approach so that neither 
checker nor developer needed to expose their IPR. On the other hand, 
since proof checkers are easier to build than proof generators, maybe 
just single-blind would do - enabling a proof developer to get his proof 
subjected to the mother of all checker hammerings wuthout exposing any IPR.

I suppose, thinking on it a bit further, that what I'm really trying to 
get at is the feasibility of a distributed proof-checking protocol that 
could preserve at least the developer's IPR.

... I'm still at the stage of blundering around to figure out what the 
question is that I really wanted to ask ... ;-)

Olwen


On 22/11/2018 16:48, Martyn Thomas wrote:
> On 22/11/2018 14:48, Olwen Morgan wrote:
>
>> Actually, after having sent this, it occurred to me that blockchain
>> technology might allow arbitrary proof-checkers to check putative
>> proofs on a double-blind anonymity basis. Perhaps this could address
>> IPR/confidentiality issues for the proof developer?
>>
>> Just a thought.
>>
>> O
>>
> I don't see the benefit of blockchain in this application, nor the need
> to be double blind. Wouldn't it be better to put the proofs somewhere
> public and have proofcheckers attach signed certificates saying they had
> checked and verified the proofs?
>
> But the problem remains that it will be necessary to show that the logic
> that the proofcheckers analyse is a correct representation of the
> software and of the claims being made about the properties of that
> software when it runs in the target environment. How would that best be
> achieved?
>
> Martyn
>
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181122/bca91711/attachment.html>