Borrowing Safe Pointers from Rust in SPARK

Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich

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-def…