2018/05/15 by Georges-Axel Jaloyan, Jaloyan, Georges-Axel, Yannick Moy +3 · 1 voice
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing #cs.PL
paper · pdf · doi:10.48550/arxiv.1805.05576
17 pages, 0 figures
arxiv created 2018/05/15 · openalex publication_date 2018/05/15 · arxiv published 2018/05/15 · arxiv updated 2018/05/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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, and enforces the Concurrent Read, Exclusive Write policy. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples. In the paper, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and compare our solution with Rust.