RE: [sc] Compiler validation ?



RE: [sc] Compiler validation ?

From: Watts Malcolm (AE/ENG11-AU) <Malcolm.Watts_at_xxxxxx>
Date: Tue, 25 Oct 2011 10:04:14 +0800
Message-ID: <B44EBD96483DB846A10BD1E7030B0E46017CFB06@xxxxxx>
Thanks to all for your comments on the compiler question.
Appreciated.

Mal.

-----Original Message-----
From: safety-critical-request@xxxxxx [mailto:safety-critical-request@xxxxxx] On Behalf Of David MENTRE
Sent: Wednesday, 19 October 2011 5:27 PM
To: safety-critical@xxxxxx
Subject: Re: [sc] Compiler validation ?

Hello,

2011/10/14 Watts Malcolm (AE/ENG11-AU) <Malcolm.Watts@xxxxxx>:
>  If no validation, how can one make the argument for confidence in the use of a compiler toolchain ?

This point has been discussed in March on this very list.

The original paper:
  http://www.cs.york.ac.uk/hise/safety-critical-archive/2011/0204.html

The thread:
  http://www.cs.york.ac.uk/hise/safety-critical-archive/2011/index.html#204

To summarize, all compilers have bugs. But some of them have much less
than others and the compcert (certified compilers programmed in Coq
proof assistant) is much promising.

Sincerely yours,
D. Mentré
Received on Tue 25 Oct 2011 - 03:05:02 BST