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.
CompCert
CompCert
You are a hit'n-run poster.
Working On:Bootloader, RWFS Image Program
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
this was a hit and run post.
Working On:Bootloader, RWFS Image Program
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
huH?
Working On:Bootloader, RWFS Image Program
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
what do you mean?
Working On:Bootloader, RWFS Image Program
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc
Leviathan: http://leviathanv.googlecode.com
Kernel:Working on Design Doc