Graph Based Reduction of Program Verification Conditions

Details Graph Based Reduction of Program Verification Conditions Graph Based Reduction of Program Verification Conditions

2009-07-08

arxiv.org/abs/0907.1357v1

Automated Formal Methods (AFM'09), colocated with CAV'09 (2009) 40-47

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Graph Based Reduction of Program Verification Conditions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Graph Based Reduction of Program Verification Conditions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Graph Based Reduction of Program Verification Conditions will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-319942