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.

#13: Rod Chapman – It's Either Automated or It's Wrong

Exploring tools and approaches that make us more effective engineers and make our systems safe and reliable. Join us for discussions on recent developments in topics such as best practices in reliability and security, applied formal methods, encryption, and safe and secure hardware.

Share #13: Rod Chapman – It's Either Automated or It's Wrong

Sign up to save your podcasts

#13: Rod Chapman – It's Either Automated or It's Wrong

#13: Rod Chapman – It's Either Automated or It's Wrong