Page 1 of 1

CompCert

Posted: Sun Apr 06, 2008 4:38 am
by binutils
Xavier Leroy wrote: The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs.
Image

Posted: Sun Apr 06, 2008 5:07 am
by inflater
Holy hell :shock: You do realize you're a spammer?

Posted: Sun Apr 06, 2008 7:07 am
by binutils
Holy no! :D

Posted: Sun Apr 06, 2008 12:19 pm
by nekros
You are a hit'n-run poster.

Posted: Mon Apr 07, 2008 9:30 am
by binutils
urm, no. maybe i would think of myself just like that about 10 years ago. :)

Posted: Mon Apr 07, 2008 9:36 am
by nekros
this was a hit and run post.

Posted: Mon Apr 07, 2008 9:48 am
by binutils
then you groupie post. :p

Posted: Mon Apr 07, 2008 9:56 am
by nekros
huH?

Posted: Mon Apr 07, 2008 10:01 am
by binutils
gang post

Posted: Mon Apr 07, 2008 10:12 am
by nekros
what do you mean?

Posted: Mon Apr 07, 2008 10:25 am
by binutils
i dunno, just came up in my mind.