As more and more complex systems are becoming safety and security critical, it is inevitable that more complex dynamic data structures will need to be verified for correctness, with bounded storage. Garbage collection has been one approach, but in a real-time multicore world, garbage collection is challenging to implement in a way that allows provable safety with bounded resources and real-time responsiveness. An alternative is a pointer storage ownership approach, which is the basis for the languages Rust and Parasail, and shows up as "unique_ptr"s in C++. Pointer storage ownership can eliminate the need for garbage collection, while providing guarantees of no dangling references and no storage leaks. This talk will present how we are adding “safe” pointers to the formally verifiable language SPARK, and what safety and resource-utilization properties we can prove formally, including in the presence of parallelism.

• Harvard College 1971-1975, AB Summa Cum Laude Chemistry
• Harvard Radcliffe Student Computing Center 1975-1979, Systems Programmer
• Intermetrics/AverStar/AverCom 1980-2002, Chief Scientist
• SofCheck 2002-2011, Founder and CTO
• AdaCore 2011-present, VP, Director of Language Research, Model-Based Toolset Product Architect