243 – Formal Specification and Proof
| Rate/Vote |   (average: 4.35) 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.
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:07
This website uses cookies to improve your experience. We'll assume you're ok with this.
Diese Webseite verwendet Cookies. Wir gehen davon aus, dass das für Sie/Dich in Ordnung ist.
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:
– https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development
– https://media.ccc.de/v/34c3-8915-how_can_you_trust_formally_verified_software
– https://media.ccc.de/v/34c3-8768-end-to-end_formal_isa_verification_of_risc-v_processors_with_riscv-formal