A provably correct embedded verifier for the certification of safety critical software

VFRAME is one of ANSALDO'S software driven vital architectures for safety critical products. This paper describes a project whose result is the development of an "embedded verifier", i.e. a system integrated within VFRAME and able to certify the correctness of one of VFRAME components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end users.