[We have episodes in German and English] How do scientists uncover phenomena and explain their connections? How do engineers design machines, methods and infrastructure? At omega tau, experts give detailed answers. Over the last ten years, we have produced 300 episodes in which we dug deeper, until we ran out of questions. Join us on our journey through the world of science and engineering: the closer you look and listen, the more interesting things get.
http://omegataupodcast.net
episode 243: Formal Specification and Proof
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
Testing vs. Proofs 01:16:19Regular expressions
Program vs Specifications 01:24:44Bubble-Sort | Quick-Sort
Real-World examples 01:29:43CompCert C | SIL4Linux | CertiKSOS | CakeML | Verified TLS | HACMS
DeepSpec 01:43:44DeepSpec Project | DeepSpec Webserver
End 01:59:07