Safe Pointers in SPARK 2014

10/19/2017
by   Georges-Axel Jaloyan, et al.
0

In the context 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 is based on static alias analysis inspired by Rust's borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write principle. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples including parts of real-life applications. Our tests show that only minor changes in the source code are required to fit the idiomatic Ada code into SPARK extended with pointers, which is a significant improvement upon the previous state of the art. The proposed extension has been approved by the Language Design Committee for SPARK for inclusion in a future version of SPARK, and is being discussed by the Ada Rapporteur Group for inclusion in the next version of Ada. In the report, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and the case studies, and compare our solution with Rust.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset