Automated Reasoning and Formal Verification
Professor Mike Gordon (University of Cambridge)
Info
|
|
Abstract
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.
Further info
|
Related series |
|
