Please use this identifier to cite or link to this item:

TitleA generalized approach to verification condition generation
Author(s)Belo Lourenco, Claudio
Frade, M. J.
Nakajima, Shin
Pinto, Jorge Sousa
KeywordsBounded model checking of software
Deductive verification
Program verification
Verification condition generator
Issue date8-Jun-2018
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
JournalProceedings - International Computer Software and Applications Conference
Abstract(s)In 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.
TypeConference paper
AccessRestricted access (UMinho)
Appears in Collections:HASLab - Artigos em atas de conferências internacionais (texto completo)

Files in This Item:
File Description SizeFormat 
  Restricted access
362,58 kBAdobe PDFView/Open

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