An Efficient VCGen-based Modular Verification of Relational Properties
Leveraging Applications of Formal Methods (ISoLA)(2024)
摘要
Deductive verification typically relies on function contracts that specify
the behavior of each function for a single function call. Relational properties
link several function calls together within a single specification. They can
express more advanced properties of a given function, such as non-interference,
continuity, or monotonicity, or relate calls to different functions, possibly
run in parallel, for instance, to show the equivalence of two implementations.
However, relational properties cannot be expressed and verified directly in the
traditional setting of modular deductive verification. Recent work proposed a
new technique for relational property verification that relies on a
verification condition generator to produce logical formulas that must be
verified to ensure a given relational property. This paper presents an overview
of this approach and proposes important enhancements. We integrate an optimized
verification condition generator and extend the underlying theory to show how
relational properties can be proved in a modular way, where one relational
property can be used to prove another one, like in modular verification of
function contracts. Our results have been fully formalized and proved sound in
the Coq proof assistant.
更多查看译文
关键词
modular verification,vcgen-based
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要