Details

Autor(en) / Beteiligte

• Jakobs, Marie-Christine
• Monahan, Rosemary
• ter Beek, Maurice H.

Titel

Reusing Predicate Precision in Value Analysis

Ist Teil von

• Integrated Formal Methods, p.63-85

Ort / Verlag

Cham: Springer International Publishing

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Software verification allows one to examine the reliability of software. Thereby, analyses exchange information to become more effective, more efficient, or to eliminate false results and increase trust in the analysis result. One type of information that analyses provide are precisions, which describe an analysis’ degree of abstraction (tracked predicates, etc.). So far, analyses mainly reuse their own precision to reverify a changed program. In contrast, we aim to reuse the precision of a predicate analysis within a value analysis. To this end, we propose 13 options to convert a predicate precision into a precision for value analysis. All options compute precisions with various degrees of abstraction and are broadly evaluated on three applications (cooperative verification, result validation, and regression verification). Also, we compare our options against using the coarsest and finest precision as well as a state-of-the-art approach for each application. Our evaluation reveals that coarser precisions work better for proof detection, while finer precisions perform better in alarm detection. Moreover, reusing a predicate precision in value analysis can be beneficial in cooperative verification and works well for validating and reverifying programs without property violations.