Graph Based Reduction of Program Verification Conditions

TL;DR

This paper introduces a graph-based method to reduce verification conditions in C program proofs by selecting relevant hypotheses, improving efficiency in industrial verification scenarios.

Contribution

It proposes a novel approach combining syntactic analysis and graph traversals to identify relevant hypotheses for verification conditions.

Findings

Effective reduction of verification conditions in industrial benchmarks

Improved proof automation efficiency

Applicable to large-scale C programs

Abstract

Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is mainly due to their size and a high number of irrelevant hypotheses. This work presents a strategy to reduce program verification conditions by selecting their relevant hypotheses. The relevance of a hypothesis is determined by the combination of a syntactic analysis and two graph traversals. The first graph is labeled by constants and the second one by the predicates in the axioms. The approach is applied on a benchmark arising in industrial program verification.