Video FOSDEM 2021: Proving heap-manipulating programs with SPARK
Channel: thindil
Date: 2021-02-24

Video FOSDEM 2021: Proving heap-manipulating programs with SPARK.
The SPARK open source proof tool for Ada now supports verifying pointer-based algorithms thanks to an ownership policy inspired by Rust.