20 January 2006
The Compcert certified compiler back-end
by GeorgesMariano
The Compcert back-end is a compiler that generates PowerPC assembly code from a low-level intermediate language called Cminor and a slightly more expressive intermediate language called Csharpminor. The particularity of this compiler is that it is written
17 January 2006
Why: a software verification tool
by GeorgesMariano
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for
16 January 2006
The contributions
by GeorgesMariano
Formal verification of an extension of a UNIX compatible, secure filesystem
1
(4 marks)
