Abstract
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.
Cite
CITATION STYLE
Cimatti, A., Giunchiglia, F., Pecchiari, P., Pietra, B., Profeta, J., Romano, D., … Yu, B. (1997). A provably correct embedded verifier for the certification of safety critical software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1254, pp. 202–213). Springer Verlag. https://doi.org/10.1007/3-540-63166-6_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
