Номер журнала: 2019.3
Заголовок статьи: Certified compiler design of predicate programs
A compiler with deductive verification facilities should be thoroughly certified to obtain high level of assurance. The development of the compiler for a predicate program using a compiler model in accordance with a model-based design method makes the compiler to be of a higher level of assurance. The main part of a compiler model is the model of inner program representation for a predicate program. The model is designed in the framework of third release of the compiler. The model architecture for inner representation of predicate program is described. Type checking is specially analyzed as an important aspect in the compiler development. The verification of the model and compiler development on the base of the model should guarantee a high level of compiler reliability.
deductive verification, program certification, model-based design
Скачать полный текст