Studying verification conditions for imperative programs

doi:10.14279/tuj.eceasst.72.1011

Utilize este identificador para referenciar este registo: https://hdl.handle.net/1822/50793

Título:	Studying verification conditions for imperative programs
Autor(es):	Lourenço, Cláudio Filipe Belo Silva Lamraoui, Si-Mohamed Nakajima, Shin Pinto, Jorge Sousa
Palavras-chave:	Verification Conditions LLVM Single-assignment form Software verification Bounded verification Single-assignment
Data:	2015
Editora:	European Association of Software Science and Technology (EASST)
Revista:	Electronic Communications of the EASST
Citação:	C.B.Lourenço, S.Lamraoui, S.Nakajima,and J.S.Pinto. Studying Verification Conditions for Imperative Programs. In G. Grov and A. Ire- land, editors, Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVOCS’15), volume 72 of Electronic Communications of the EASST, 2015. European Association of Software Science and Technology.
Resumo(s):	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.
Tipo:	Artigo
URI:	https://hdl.handle.net/1822/50793
DOI:	10.14279/tuj.eceasst.72.1011
ISSN:	1863-2122
Arbitragem científica:	yes
Acesso:	Acesso aberto
Aparece nas coleções:	HASLab - Artigos em atas de conferências internacionais (texto completo)