Go offline with the Player FM app!
243 - Formal Specification and Proof
Manage episode 176729155 series 26357
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.
Introduction of Benjamin C. Pierce
00:02:14Benjamin Pierce at the University of Pennsylvania | Benjamin's Book, Software Foundations | SPLASH Conference
Intro to the topic
00:03:09Critical infrastructure | Complexity | Modular programming | Compiler | C programming language | C++ programming language | Buffer overflow | Correctness | Semantics | Unit-Testing | Formal specification | Test coverage
Formal Specifications
00:26:12Formal Specifications | x86 | SMT solvers | SAT solvers | Proof assistants | Induction
Dependent types
00:58:54Dependant types | Curry–Howard correspondence | Haskell programming language | Generalized algebraic data type
Other uses of Formal Specifications
01:05:14Model based testing | Csmith | POSIX | TCP Protocol Stack | PowerPC | ARM architecture | OmegaTau about domain specific languages (german) | Interpreter
End
01:59:07410 episodes
Manage episode 176729155 series 26357
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.
Introduction of Benjamin C. Pierce
00:02:14Benjamin Pierce at the University of Pennsylvania | Benjamin's Book, Software Foundations | SPLASH Conference
Intro to the topic
00:03:09Critical infrastructure | Complexity | Modular programming | Compiler | C programming language | C++ programming language | Buffer overflow | Correctness | Semantics | Unit-Testing | Formal specification | Test coverage
Formal Specifications
00:26:12Formal Specifications | x86 | SMT solvers | SAT solvers | Proof assistants | Induction
Dependent types
00:58:54Dependant types | Curry–Howard correspondence | Haskell programming language | Generalized algebraic data type
Other uses of Formal Specifications
01:05:14Model based testing | Csmith | POSIX | TCP Protocol Stack | PowerPC | ARM architecture | OmegaTau about domain specific languages (german) | Interpreter
End
01:59:07410 episodes
All episodes
×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.