Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Deductive Verification with the Help of Abstract Interpretation

Abstract : Abstract interpretation is widely used in static analysis tools. However, to the best of our knowledge, it has not been extensively experimented in an interactive deductive verification context. This paper describes an analysis by abstract interpretation to infer loop invariants in the Why3 tool. The analysis takes advantage of the logic annotations present in the source code, including potential handwritten loop invariants. The inferred invariants are added to loops as if written by the user. They are checked by external provers and thus the analysis by abstract interpretation does not need to be trusted. Our analysis goes beyond numerical invariants. We describe two functors that add uninterpreted functions and quantifiers to a numerical abstract domain. The resulting domain is generic enough to reason about algebraic types, Booleans, or arrays. We show that it achieves a level of expressivity comparable to that of ad-hoc domains for arrays found in the literature.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01634318
Contributor : Lucas Baudin <>
Submitted on : Monday, November 13, 2017 - 11:44:43 PM
Last modification on : Tuesday, May 4, 2021 - 2:06:01 PM
Long-term archiving on: : Wednesday, February 14, 2018 - 3:28:56 PM

File

imarticle.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01634318, version 1

Collections

Citation

Lucas Baudin. Deductive Verification with the Help of Abstract Interpretation. 2017. ⟨hal-01634318⟩

Share

Metrics

Record views

339

Files downloads

218