DocumentCode
129059
Title
Property directed invariant refinement for program verification
Author
Welp, Tobias ; Kuehlmann, Andreas
Author_Institution
Univ. of California at Berkeley, Berkeley, CA, USA
fYear
2014
fDate
24-28 March 2014
Firstpage
1
Lastpage
6
Abstract
We present a novel, sound, and complete algorithm for deciding safety properties in programs with static memory allocation. The new algorithm extends the program verification paradigm using loop invariants presented in [1] with a counterexample guided abstraction refinement (CEGAR) loop [2] where the refinement is achieved by strengthening loop invariants using the QFBV generalization of Property Directed Reachability (PDR) discussed in [3, 4]. We compare the algorithm with other approaches to program verification and report experimental results.
Keywords
embedded systems; program control structures; program verification; storage allocation; QF BV generalization; counterexample guided abstraction refinement loop; loop invariants; program verification paradigm; property directed invariant refinement; property directed reachability; static memory allocation; Abstracts; Algorithm design and analysis; Bismuth; Interpolation; Resource management; Safety; Software;
fLanguage
English
Publisher
ieee
Conference_Titel
Design, Automation and Test in Europe Conference and Exhibition (DATE), 2014
Conference_Location
Dresden
Type
conf
DOI
10.7873/DATE.2014.127
Filename
6800328
Link To Document