Skip to main content

Automated Reasoning and Formal Verification

Professor Mike Gordon ( University of Cambridge )

There are many ways to use automated reasoning in the verification of computer systems. These range from heroic user guided proofs of correctness in powerful formal specification languages, to automatic checking of decidable properties in propositional logics.

I'll describe some traditional and some novel applications of theorem proving, taken from recent research at Cambridge, and then discuss a number of general issues that the examples raise.

Share this: