Artwork

Content provided by Markus Voelter and Nora Ludewig. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Markus Voelter and Nora Ludewig or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://player.fm/legal.
Player FM - Podcast App
Go offline with the Player FM app!

243 - Formal Specification and Proof

2:02:51
 
Share
 

Manage episode 176729155 series 26357
Content provided by Markus Voelter and Nora Ludewig. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Markus Voelter and Nora Ludewig or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://player.fm/legal.

Guest: Benjamin Pierce Host: Markus Voelter Shownoter: Bastian Hundt

The increasing complexity of software requires increasingly sophisticated means of ensuring its correctness — “just” testing is not necessarily good enough, depending on the domain in which the software is used. Formal specification, verification and proof is a field with a long tradition in computer science that is gaining more (practical) relevance these days; and in this episode, we cover the basics. Our guest is Benjamin Pierce, professor of computer science at UPenn. We discuss the nature of (good) specifications, how verification and proof is different from testing, and where and how these techniques are successfully used today.

For further details, you might want to check out Benjamin’s (free online) book Software Foundations.

Dependent types

00:58:54

Dependant types | Curry–Howard correspondence | Haskell programming language | Generalized algebraic data type

Testing vs. Proofs

01:16:19

Regular expressions

Program vs Specifications

01:24:44

Bubble-Sort | Quick-Sort

Real-World examples

01:29:43

CompCert C | SIL4Linux | CertiKSOS | CakeML | Verified TLS | HACMS

End

01:59:07

  continue reading

410 episodes

Artwork
iconShare
 
Manage episode 176729155 series 26357
Content provided by Markus Voelter and Nora Ludewig. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Markus Voelter and Nora Ludewig or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://player.fm/legal.

Guest: Benjamin Pierce Host: Markus Voelter Shownoter: Bastian Hundt

The increasing complexity of software requires increasingly sophisticated means of ensuring its correctness — “just” testing is not necessarily good enough, depending on the domain in which the software is used. Formal specification, verification and proof is a field with a long tradition in computer science that is gaining more (practical) relevance these days; and in this episode, we cover the basics. Our guest is Benjamin Pierce, professor of computer science at UPenn. We discuss the nature of (good) specifications, how verification and proof is different from testing, and where and how these techniques are successfully used today.

For further details, you might want to check out Benjamin’s (free online) book Software Foundations.

Dependent types

00:58:54

Dependant types | Curry–Howard correspondence | Haskell programming language | Generalized algebraic data type

Testing vs. Proofs

01:16:19

Regular expressions

Program vs Specifications

01:24:44

Bubble-Sort | Quick-Sort

Real-World examples

01:29:43

CompCert C | SIL4Linux | CertiKSOS | CakeML | Verified TLS | HACMS

End

01:59:07

  continue reading

410 episodes

All episodes

×
 
Loading …

Welcome to Player FM!

Player FM is scanning the web for high-quality podcasts for you to enjoy right now. It's the best podcast app and works on Android, iPhone, and the web. Signup to sync subscriptions across devices.

 

Quick Reference Guide