|
|
|
|
|
|
by reirob
56 days ago
|
|
|
Right from https://www.adacore.com/languages/spark, under the title Memory Safety: Through a combination of mitigation of dynamic memory usage, borrow-checking analysis and advanced formal proof, SPARK formally demonstrates absence of memory issues such as use after free, access to uninitialized memory or memory leaks and corruption. |
|
|