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.
Watch all our episodes on the Building Better Systems youtube channel.
Joey Dodds: https://galois.com/team/joey-dodds/
Shpat Morina: https://galois.com/team/shpat-morina/
Rod Chapman: linkedin.com/in/rod-chapman-7b60266
https://github.com/rod-chapman/SPARKNaCl
Galois, Inc.: https://galois.com/
Contact us: [email protected]
Fler avsnitt av Building Better Systems
Visa alla avsnitt av Building Better SystemsBuilding Better Systems med Galois, Joey Dodds, Shpat Morina finns tillgänglig på flera plattformar. Informationen på denna sida kommer från offentliga podd-flöden.
