Property Directed Invariant Refinement For Program Verification

Proceedings of the conference on Design, Automation & Test in Europe（2014）

引用 1|浏览0

暂无评分

摘要

We present a novel, sound, and complete algorithm for deciding safety properties in programs with static memory allocation. The new algorithm extends the program verification paradigm using loop invariants presented in [1] with a counterexample guided abstraction refinement (CEGAR) loop [2] where the refinement is achieved by strengthening loop invariants using the QF_BV generalization of Property Directed Reachability (PDR) discussed in [3, 4]. We compare the algorithm with other approaches to program verification and report experimental results.

查看译文

关键词

embedded systems,program control structures,program verification,storage allocation,QF BV generalization,counterexample guided abstraction refinement loop,loop invariants,program verification paradigm,property directed invariant refinement,property directed reachability,static memory allocation,

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要