Artwork

Вміст надано Galois Inc., Joey Dodds, and Shpat Morina. Весь вміст подкастів, включаючи епізоди, графіку та описи подкастів, завантажується та надається безпосередньо компанією Galois Inc., Joey Dodds, and Shpat Morina або його партнером по платформі подкастів. Якщо ви вважаєте, що хтось використовує ваш захищений авторським правом твір без вашого дозволу, ви можете виконати процедуру, описану тут https://uk.player.fm/legal.
Player FM - додаток Podcast
Переходьте в офлайн за допомогою програми Player FM !

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

44:03
 
Поширити
 

Manage episode 303134175 series 2824530
Вміст надано Galois Inc., Joey Dodds, and Shpat Morina. Весь вміст подкастів, включаючи епізоди, графіку та описи подкастів, завантажується та надається безпосередньо компанією Galois Inc., Joey Dodds, and Shpat Morina або його партнером по платформі подкастів. Якщо ви вважаєте, що хтось використовує ваш захищений авторським правом твір без вашого дозволу, ви можете виконати процедуру, описану тут https://uk.player.fm/legal.

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: podcast@galois.com

  continue reading

22 епізодів

Artwork
iconПоширити
 
Manage episode 303134175 series 2824530
Вміст надано Galois Inc., Joey Dodds, and Shpat Morina. Весь вміст подкастів, включаючи епізоди, графіку та описи подкастів, завантажується та надається безпосередньо компанією Galois Inc., Joey Dodds, and Shpat Morina або його партнером по платформі подкастів. Якщо ви вважаєте, що хтось використовує ваш захищений авторським правом твір без вашого дозволу, ви можете виконати процедуру, описану тут https://uk.player.fm/legal.

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: podcast@galois.com

  continue reading

22 епізодів

Усі епізоди

×
 
Loading …

Ласкаво просимо до Player FM!

Player FM сканує Інтернет для отримання високоякісних подкастів, щоб ви могли насолоджуватися ними зараз. Це найкращий додаток для подкастів, який працює на Android, iPhone і веб-сторінці. Реєстрація для синхронізації підписок між пристроями.

 

Короткий довідник