Studying Verification Conditions for Imperative Programs

Cláudio Belo Lourenço; Si-Mohamed Lamraoui; Shin Nakajima; Jorge Sousa Pinto

doi:10.14279/tuj.eceasst.72.1011

Studying Verification Conditions for Imperative Programs

Authors

Cláudio Belo Lourenço HASLab/INESC TEC & Universidade do Minho, Portugal
Si-Mohamed Lamraoui National Institute of Informatics, Japan
Shin Nakajima National Institute of Informatics, Japan
Jorge Sousa Pinto HASLab/INESC TEC & Universidade do Minho, Portugal

DOI:

https://doi.org/10.14279/tuj.eceasst.72.1011

Abstract

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.

Downloads

Published

2015-11-25

How to Cite

[1]

C. Belo Lourenço, S.-M. Lamraoui, S. Nakajima, and J. Sousa Pinto, “Studying Verification Conditions for Imperative Programs”, eceasst, vol. 72, Nov. 2015.