Artwork

Treść dostarczona przez Galois Inc., Joey Dodds, and Shpat Morina. Cała zawartość podcastów, w tym odcinki, grafika i opisy podcastów, jest przesyłana i udostępniana bezpośrednio przez Galois Inc., Joey Dodds, and Shpat Morina lub jego partnera na platformie podcastów. Jeśli uważasz, że ktoś wykorzystuje Twoje dzieło chronione prawem autorskim bez Twojej zgody, możesz postępować zgodnie z procedurą opisaną tutaj https://pl.player.fm/legal.
Player FM - aplikacja do podcastów
Przejdź do trybu offline z Player FM !

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

44:03
 
Udostępnij
 

Manage episode 303134175 series 2824530
Treść dostarczona przez Galois Inc., Joey Dodds, and Shpat Morina. Cała zawartość podcastów, w tym odcinki, grafika i opisy podcastów, jest przesyłana i udostępniana bezpośrednio przez Galois Inc., Joey Dodds, and Shpat Morina lub jego partnera na platformie podcastów. Jeśli uważasz, że ktoś wykorzystuje Twoje dzieło chronione prawem autorskim bez Twojej zgody, możesz postępować zgodnie z procedurą opisaną tutaj https://pl.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 odcinków

Artwork
iconUdostępnij
 
Manage episode 303134175 series 2824530
Treść dostarczona przez Galois Inc., Joey Dodds, and Shpat Morina. Cała zawartość podcastów, w tym odcinki, grafika i opisy podcastów, jest przesyłana i udostępniana bezpośrednio przez Galois Inc., Joey Dodds, and Shpat Morina lub jego partnera na platformie podcastów. Jeśli uważasz, że ktoś wykorzystuje Twoje dzieło chronione prawem autorskim bez Twojej zgody, możesz postępować zgodnie z procedurą opisaną tutaj https://pl.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 odcinków

Все серии

×
 
Loading …

Zapraszamy w Player FM

Odtwarzacz FM skanuje sieć w poszukiwaniu wysokiej jakości podcastów, abyś mógł się nią cieszyć już teraz. To najlepsza aplikacja do podcastów, działająca na Androidzie, iPhonie i Internecie. Zarejestruj się, aby zsynchronizować subskrypcje na różnych urządzeniach.

 

Skrócona instrukcja obsługi