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

Registo completo

Campo DC	Valor	Idioma
dc.contributor.author	Lourenço, Cláudio Filipe Belo Silva	por
dc.contributor.author	Lamraoui, Si-Mohamed	por
dc.contributor.author	Nakajima, Shin	por
dc.contributor.author	Pinto, Jorge Sousa	por
dc.date.accessioned	2018-02-21T14:50:37Z	-
dc.date.available	2018-02-21T14:50:37Z	-
dc.date.issued	2015	-
dc.identifier.citation	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.	por
dc.identifier.issn	1863-2122	-
dc.identifier.uri	https://hdl.handle.net/1822/50793	-
dc.description.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.	por
dc.description.sponsorship	This work is partially financed by the FCT – Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project UID/EEA/50014/2013 and by the NII International Internship Program.	por
dc.description.sponsorship	SFRH/BD/52236/2013	por
dc.language.iso	eng	por
dc.publisher	European Association of Software Science and Technology (EASST)	por
dc.relation	info:eu-repo/grantAgreement/FCT/5876/147326/PT	por
dc.rights	openAccess	por
dc.rights.uri	http://creativecommons.org/licenses/by/4.0/	por
dc.subject	Verification Conditions	por
dc.subject	LLVM	por
dc.subject	Single-assignment form	por
dc.subject	Software verification	por
dc.subject	Bounded verification	por
dc.subject	Single-assignment	por
dc.title	Studying verification conditions for imperative programs	por
dc.type	article	por
dc.peerreviewed	yes	por
oaire.citationStartPage	1	por
oaire.citationEndPage	15	por
oaire.citationVolume	72	por
dc.identifier.doi	10.14279/tuj.eceasst.72.1011	por
dc.subject.fos	Ciências Naturais::Ciências da Computação e da Informação	por
dc.description.publicationversion	info:eu-repo/semantics/publishedVersion	por
sdum.journal	Electronic Communications of the EASST	por
sdum.conferencePublication	Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVOCS’15)	por
Aparece nas coleções:	HASLab - Artigos em atas de conferências internacionais (texto completo)