Re: [SystemSafety] Claims for formal methods

From: David MENTRE < >
Date: Thu, 20 Feb 2014 10:16:58 +0100

Hello Mr. Jones,

Le 19/02/2014 11:59, Derek M Jones a écrit :
>> Please provide some examples (preferably from peer-reviewed
>> journals) of the "excessive claims" that you are criticising.
> There are the articles discussed in links I posted to the original
> thread:
> The French group in the above links did some interesting work on
> compiler code generation and I believe they now refer to it as a
> verified compiler backend (which is what it idoes) rather than a
> verified C compiler.

They are doing more than just a C backend and they are progressing slowly but surely towards parsing the C grammar. For example, you can have a look at this work:

Above work is dated end of 2012. I don't know if it has been integrated within currently released ComptCert ( or not.

Regarding the points you raised:
> 1. C source code is not verified directly, it is first translated
> to the formal notations used by the verification system; the software
> that performs this translation is assumed to be correct.

True. But as I said above, they are working on it.

> 2. The CompCert system may successfully translate programs
> containing undefined behavior. Any proof statements made about such
> programs may not be valid.

Yes. But this is not the issue with the Verified C compiler but with the input C program itself. You can use other tools (like Frama-C, Astrée or Polyspace) to check your C program has no undefined behaviour.

> 3. The support tools are assumed to be correct; primarily the Coq
> proof assistant, which is written in OCaml.

Yes. But Coq is designed in such a way (a very small, manually verified trusted core and then libraries built upon that core) that the possibility to have an issue in Coq is very very low (but not zero, I agree).

Regarding OCaml, yes some bugs in the OCaml compiler or run-time could theoretically impact Coq. But having such bugs is very remote. And some people (Esterel Technologies people for SCADE compiler) have developed a simplified OCaml run-time to fulfil DO178B criteria (see "Certified Development Tools Implementation in Objective Caml". Pagano, Andrieu, et al. PADL 2008, LNCS 4902).

> 4. The CompCert system makes decisions about implementation
> dependent behaviors and any proofs only apply in the context of these
> decisions.

Yes. As any compiler. At least those decisions are formally documented.

> 5; The CompCert system makes decisions about unspecified behaviors
> and any proofs only apply in the context of these decisions.

Yes. As any compiler. At least those decisions are formally documented.

As pointed out on the comment of your blog, an independent research paper ( has shown that ComptCert is a very strong compiler, much stronger that any others. Quoting Regehr's paper:
The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users. """

I've read somewhere (sorry, no precise reference), that the parts where bugs were found in Regehr's paper have been formalized since then.

Sincerely yours,
D. Mentré

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Feb 20 2014 - 10:17:13 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST