This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)
Abstract
The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.