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

Registo completo
Campo DCValorIdioma
dc.contributor.authorBelo Lourenco, Claudiopor
dc.contributor.authorFrade, M. J.por
dc.contributor.authorNakajima, Shinpor
dc.contributor.authorPinto, Jorge Sousapor
dc.date.accessioned2020-08-03T11:27:11Z-
dc.date.issued2018-06-08-
dc.identifier.isbn9781538626665por
dc.identifier.issn0730-3157-
dc.identifier.urihttps://hdl.handle.net/1822/66208-
dc.description.abstractIn a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns.por
dc.description.sponsorshipChina National Funds for Distinguished Young Scientists (POCI-01-0145-FEDER-006961’)por
dc.language.isoengpor
dc.publisherInstitute of Electrical and Electronics Engineers (IEEE)por
dc.rightsrestrictedAccesspor
dc.subjectBounded model checking of softwarepor
dc.subjectDeductive verificationpor
dc.subjectProgram verificationpor
dc.subjectVerification condition generatorpor
dc.titleA generalized approach to verification condition generationpor
dc.typeconferencePaperpor
dc.peerreviewedyespor
oaire.citationStartPage194por
oaire.citationEndPage203por
oaire.citationVolume1por
dc.date.updated2020-08-03T11:02:26Z-
dc.identifier.doi10.1109/COMPSAC.2018.00032por
dc.date.embargo10000-01-01-
sdum.export.identifier5714-
sdum.journalProceedings - International Computer Software and Applications Conferencepor
oaire.versionAMpor
Aparece nas coleções:HASLab - Artigos em atas de conferências internacionais (texto completo)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
2018_COMPSAC_18.pdf
Acesso restrito!
362,58 kBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID