243 – Formal Specification and Proof

Rate Episode
(average: 4.47)
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

00:26:12

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

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

DeepSpec

01:43:44

DeepSpec Project | DeepSpec Webserver

End

01:59:07

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