Skip to Main content Skip to Navigation
Conference papers

Verification of Programs with Pointers in SPARK

Abstract : In the field of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution uses a permission-based static alias analysis method inspired by Rust's borrow-checker and affine types. To validate our approach, we have implemented it in the SPARK GNATprove formal verification toolset for Ada. In the paper, we give a formal presentation of the analysis rules for a core version of SPARK and discuss their implementation and scope.
Document type :
Conference papers
Complete list of metadata
Contributor : Andrei Paskevich Connect in order to contact the contributor
Submitted on : Monday, January 4, 2021 - 1:00:34 PM
Last modification on : Wednesday, January 26, 2022 - 3:14:14 AM
Long-term archiving on: : Monday, April 5, 2021 - 8:02:56 PM


Files produced by the author(s)



Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich. Verification of Programs with Pointers in SPARK. ICFEM 2020 - 22nd International Conference on Formal Engineering Methods, Mar 2020, Singapore / Virtual, Singapore. pp.55-72, ⟨10.1007/978-3-030-63406-3_4⟩. ⟨hal-03094566⟩



Les métriques sont temporairement indisponibles