n/a
}, pages = {194{\textendash}203}, publisher = {{IEEE} Computer Society}, organization = {{IEEE} Computer Society}, abstract = {In a world where many human lives depend on the correct behavior of software systems, program verification as- sumes 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.
}, doi = {10.1109/COMPSAC.2018.00032}, url = {https://doi.org/10.1109/COMPSAC.2018.00032}, attachments = {https://haslab.uminho.pt/sites/default/files/mjf/files/main.pdf}, author = {Cl{\'a}udio Belo Louren{\c c}o and Maria Jo{\~a}o Frade and Shin Nakajima and Jorge Sousa Pinto}, editor = {Sorel Reisman and Sheikh Iqbal Ahamed and Claudio Demartini and Thomas M. Conte and Ling Liu and William R. Claycomb and Motonori Nakamura and Edmundo Tovar and Stelvio Cimato and Chung{-}Horng Lung and Hiroki Takakura and Ji{-}Jiang Yang and Toyokazu Akiyama and Zhiyong Zhang and Kamrul Hasan} }