Applying High-Level Function Loop Invariants for Machine Code Deductive Verification

The existing tools of deductive verification allow us to successfully prove the correctness of functions written in high-level languages such as C or Java. However, this may not be enough for critical software because even fully verified code cannot guarantee the correct generation of machine code b...

全面介紹

書目詳細資料

發表在:	Труды Института системного программирования РАН
主要作者:	Pavel Andreevitch Putro
格式:	Article
語言:	英语
出版:	Russian Academy of Sciences, Ivannikov Institute for System Programming 2019-09-01
主題:	дедуктивная верификация формальные методы машинный код
在線閱讀:	https://ispranproceedings.elpub.ru/jour/article/view/1166