Paper Info
Title
Safe Dynamic Memory Management In Ada And Spark
Abstract
Handling memory in a correct and efficient way is a step toward safer, less complex, and higher performing software-intensive systems. However, languages used for critical software development such as Ada, which supports formal verification with its SPARK subset, face challenges regarding any use of pointers due to potential pointer aliasing. In this work, we introduce an extension to the Ada language, and to its SPARK subset, to provide pointer types ("access types" in Ada) that provide provably safe, automatic storage management without any asynchronous garbage collection, and without explicit deallocation by the user. Because the mechanism for these safe pointers relies on strict control of aliasing, it can be used in the SPARK subset for formal verification, including both information flow analysis and proof of safety and correctness properties. In this paper, we present this proposal (which has been submitted for inclusion in the next version of Ada), and explain how we are able to incorporate these pointers into formal analyses.
Year
DOI
Venue
2018
10.1007/978-3-319-92432-8_3
RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2018
Keywords
Field
DocType
Compilation, Safe pointers, Formal verification, Memory management
Pointer (computer programming),Spark (mathematics),Programming language,Computer science,Correctness,Pointer aliasing,Memory management,Garbage collection,Software development,Formal verification
Conference
Volume
ISSN
Citations 
10873
0302-9743
0
PageRank 
References 
Authors
0.34
5
3
Name
Order
Citations
PageRank
Maroua Maalej100.34
S. Tucker Taft25014.12
Yannick Moy3699.25