Re: [Rodin-b-sharp-user] Soundness

[Matthias S. <Mat...@in...>]

Hi Karim,

Rodin's external provers do not output proofs or certificates and 
therefore need to be trusted. Occasionally, these provers have been 
unsound. See the Rodin bug tracker for more information.

-Matthias

Am 19.10.2011 17:12, schrieb karim kanso:
> Hello,
>
> Im new to the RODIN platform and was wondering if anyone could point me
> in the right
> direction where I can find information relating to the soundness of the
> integration of external
> provers. What assurances does RODIN come with that the proofs are valid,
> e.g. does it check
> the correctness of traces produced by the external tools, are the tools
> certified/verified?
>
> Ive searched the wiki, but have found very little mention of the
> soundness of external tools.
>
>
> Thanks,
> Karim Kanso
> Swansea University
>
>
>
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2d-oct
>
>
>
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user