Mechanically-checked soundness of type-based null safety
Null pointer dereferencing remains one of the major source of bugs in software. This presentation reviews the first mechanically-checked formalization of guaranteed null safety based on the notion of free and committed types in a statically-typed object-oriented language. It summarizes the results of translation from the original proof on paper into Isabelle/HOL, discusses found inconsistencies, implicit assumptions, and genuine mistakes, and reports on the completed proof for the extended type system.
|Pre-recorded video (CPP-2021 Mechanically-checked soundness of type-based null safety.mkv)||15.59MiB|