文章基本信息

标题：Studying Verification Conditions for Imperative Programs
本地全文：下载
作者：Cláudio Belo Lourenço ; Si-Mohamed Lamraoui ; Shin Nakajima 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2015
卷号：72
DOI：10.14279/tuj.eceasst.72.1011
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：Program verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with experimental results originated by verification conditions generated from the intermediate representation of LLVM.
其他摘要：Program verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with experimental results originated by verification conditions generated from the intermediate representation of LLVM.