Exploiting Pointer Analysis in Memory Models for Deductive Verification
Exploiting Pointer Analysis in Memory Models for Deductive Verification
复制标题
利用内存模型中的指针分析进行演绎验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Boris Yakobowski
中科院分区：
文献类型：
--
作者：
Quentin Bouillaguet;François Bobot;M. Sighireanu;Boris Yakobowski
验证方法之间的协作对于解决软件验证这一具有挑战性的问题至关重要。本文主要研究C程序的指针验证，形式化地描述了进行指针分析的静态分析器与基于一阶逻辑的演绎验证工具之间的协作。我们提出了一个基于内存模型的框架，该框架捕获了指针分析所推断的内存划分，并遵循用于生成验证条件的内存模型。该框架指导我们提出了一种指针分析，该分析适应于指针上的各种低级操作，同时为演绎验证提供了关于内存分区的准确信息。我们在FRAMA-C平台中实现了这种协作，并在一个复杂的案例研究中展示了它在减少演绎验证任务方面的有效性。
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer analysis and a deductive verification tool based on first order logic. We propose a framework based on memory models that captures the partitioning of memory inferred by pointer analyses, and complies with the memory models used to generate verification conditions. The framework guided us to propose a pointer analysis that accommodates to various low-level operations on pointers while providing precise information about memory partitioning to the deductive verification. We implemented this cooperation inside the Frama-C platform and we show its effectiveness in reducing the task of deductive verification on a complex case study.
DOI：
10.1016/j.scico.2010.07.004
发表时间：
2012-08
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin
通讯作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin