Video FOSDEM 2021: Proving heap-manipulating programs with SPARK.The SPARK open source proof tool for Ada now supports verifying pointer-based algorithms tha...