Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations.
Podden och tillhörande omslagsbild på den här sidan tillhör Galois, Joey Dodds, Shpat Morina. Innehållet i podden är skapat av Galois, Joey Dodds, Shpat Morina och inte av, eller tillsammans med, Poddtoppen.
