Region analysis for deductive verification of C programs


如何引用文章

全文:

开放存取 开放存取
受限制的访问 ##reader.subscriptionAccessGranted##
受限制的访问 订阅存取

详细

This paper presents a memory model with nonoverlapping memory areas (regions) for the deductive verification of C programs. This memory model uses a core language that supports arbitrary nesting of structures, unions, and arrays into other structures and allows reducing the number of user-provided annotations as a result of region analysis. This paper also describes semantics of the core language and normalizing transformations for translating an input annotated C program into a program in the core language. In addition, an encoding is proposed for modeling the memory state of a core-language program with logical formulas as described by the model semantics of the core language. For the model semantics, the soundness and completeness theorems are proved. Additional constraints on the typing context of the core-language terms are described that determine the result of the region analysis enabling the complete modeling of a limited class of programs without using additional annotations. A proof sketch for the theorem stating completeness of the proposed region analysis for a limited class of programs is presented.

作者简介

M. Mandrykin

Institute for System Programming

编辑信件的主要联系方式.
Email: mandrykin@ispras.ru
俄罗斯联邦, ul. Solzhenitsyna 25, Moscow, 109004

A. Khoroshilov

Institute for System Programming; Moscow State University; Moscow Institute of Physics and Technology; National Research University Higher School of Economics

Email: mandrykin@ispras.ru
俄罗斯联邦, ul. Solzhenitsyna 25, Moscow, 109004; Moscow, 119991; Institutskii per. 9, Dolgoprudnyi, Moscow oblast, 141700; ul. Myasnitskaya 20, Moscow, 101000

补充文件

附件文件
动作
1. JATS XML

版权所有 © Pleiades Publishing, Ltd., 2016