Robert L. Constable
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."