Synthesis of Annotations for Partially Automated Deductive Verification

Abstract: We investigate the possibility of inferring annotations from source code to enable a partially automated process of deductive verification within the scope of embedded systems code. Specifically, we design a plugin for the verification framework Frama-C, that synthesizes function contracts including every precondition necessary to later prove functional software specifications. We decouple what we referred to as auxiliary annotations from functional specifications, and to our knowledge, we provide the first work that synthesizes all auxiliary annotations, using only information present in source code. We make multiple contributions: we create a plugin for Frama-C, we test the quality of generated annotations on industrial embedded code that is used in leading heavy vehicle products, and we describe in detail how such a plugin can be realized. Our results indicate that inference of annotations within this scope is feasible and useful.