Towards deductive verification of C programs with shared data

详细信息    查看全文

• 作者：M. U. Mandrykin ; A. V. Khoroshilov
• 刊名：Programming and Computer Software
• 出版年：2016
• 出版时间：September 2016
• 年：2016
• 卷：42
• 期：5
• 页码：324-332
• 全文大小：830 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 considers the problem of the deductive verification of the Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow applying traditional deductive verification techniques, so we consider how to verify such a code by proving its compliance to a given specification of a certain synchronization discipline. The approach is illustrated by the examples of a spinlock specification and a simplified specification of the read-copy-update (RCU) API.