243 – Formal Specification and Proof

Rate Episode
(average: 4.40)
Loading ... Loading ...

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.

Formal Specifications


Formal Specifications | x86 | SMT solvers | SAT solvers | Proof assistants | Induction

Dependent types


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

Testing vs. Proofs


Regular expressions

Program vs Specifications


Bubble-Sort | Quick-Sort

Real-World examples


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



DeepSpec Project | DeepSpec Webserver



Cite this Episode / Zitiere diese Episode
Embedded Audio Player  |  Bibtex Entry  |  Text