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
Contributor : Lucas Baudin Connect in order to contact the contributor
Submitted on : Monday, November 13, 2017 - 11:44:43 PM
Last modification on : Thursday, March 17, 2022 - 10:08:35 AM
Long-term archiving on: : Wednesday, February 14, 2018 - 3:28:56 PM


Files produced by the author(s)


  • HAL Id : hal-01634318, version 1



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



Record views


Files downloads