Dean of Faculty of Computing and Information Science, Professor of Computer Science Cornell University
Thirty Years of Progress in Formal Methods
Edmund Clarke graduated from Cornell thirty years ago. This
talk will examine progress in the area of formal methods to which Ed Clarke
has made so many fundamental contributions in model checking, theorem proving
and basic theory. It will consider Ed's influence on Cornell research and the
world wide context he created for work in formal methods.
I will present one new technical result showing that it is possible to automatically extract distributed systems from constructive proofs that specifications in a Logic of Events are achievable. This is joint work with Mark Bickford of the ATC-NY corporation. The formal proofs use model checking and the specification language includes temporal operators integrated into computational type theory with a type of Events. The Logic of Events is exceptionally abstract, yet as the extraction results show, not "too abstract."