Region analysis for deductive verification of C programs

详细信息    查看全文

• 作者：M. U. Mandrykin ; A. V. Khoroshilov
• 刊名：Programming and Computer Software
• 出版年：2016
• 出版时间：September 2016
• 年：2016
• 卷：42
• 期：5
• 页码：257-278
• 全文大小：2,910 KB
• 刊物类别：Computer Science
• 刊物主题：Computer Science, general
  Software Engineering, Programming and Operating Systems
  Operating Systems
  Software Engineering
  Artificial Intelligence and Robotics
  Russian Library of Science
  
• 出版者：MAIK Nauka/Interperiodica distributed exclusively by Springer Science+Business Media LLC.
• ISSN：1608-3261
• 卷排序：42

文摘

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.