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. Pierce00:02:14
Benjamin Pierce at the University of Pennsylvania | Benjamin's Book, Software Foundations | SPLASH Conference
Intro to the topic00:03:09
Critical infrastructure | Complexity | Modular programming | Compiler | C programming language | C++ programming language | Buffer overflow | Correctness | Semantics | Unit-Testing | Formal specification | Test coverage
Formal Specifications | x86 | SMT solvers | SAT solvers | Proof assistants | Induction
Dependant types | Curry–Howard correspondence | Haskell programming language | Generalized algebraic data type
Other uses of Formal Specifications01:05:14
Model based testing | Csmith | POSIX | TCP Protocol Stack | PowerPC | ARM architecture | OmegaTau about domain specific languages (german) | Interpreter
Testing vs. Proofs01:16:19
Program vs Specifications01:24:44
CompCert C | SIL4Linux | CertiKSOS | CakeML | Verified TLS | HACMS
Thanks for another very interesting episode. Pierce is a very good speaker, and Markus had enough knowledge to ask good questions. One quibble: Integration of fully automatic provers into interactive proof assistants (“Hammering”, after Larry Paulson’s “Sledgehammer” in Isabelle) is one of the core technologies that make large-scale verification possible. But the provers used in hammering are not primarily SAT or SMT solvers (though these are increasingly also being used), but classical first-order provers like E, Vampire, or SPASS.
Hello and thanks for this interesting episode :-)
It’s always fun to peak into a topic one never even knew existed. Because of that, I noticed that several related talks/presentations have been held about 8 month after this episode at the 34th Chaos Communication Congress: