Skip to Main content Skip to Navigation
Conference papers

Verication of Programs with Pointers in SPARK

Abstract : In the field of deductive software verication, 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 metadatas

https://hal.inria.fr/hal-03094566
Contributor : Andrei Paskevich <>
Submitted on : Monday, January 4, 2021 - 1:00:34 PM
Last modification on : Monday, January 18, 2021 - 1:52:02 PM

File

ICFEM20_paper_5.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich. Verication of Programs with Pointers in SPARK. ICFEM 2020: Formal Methods and Software Engineering, Mar 2021, Singapore, Singapore. pp.55-72, ⟨10.1007/978-3-030-63406-3_4⟩. ⟨hal-03094566⟩

Share

Metrics

Record views

16

Files downloads

79