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."