Center for Formal Methods

Introduction

The idea that computer programs and computer hardware should be verified to meet their specification by formal logical methods, including computer generated and computer-checked proofs of correctness goes back at least to 1961. However, neither the need nor the methods existed at first. Also the number of mathematicians, logicians and computer scientists inferested in formal verification was very small.

Over the years, all three of these situations have changed.

Hardware and software systems have become enormously larger and more complex. The time spent in trying to verify them has grown to a substantial part of the whole development effort. Verification now imposes substantial delays before a product is ready for market. Costly errors often remain even after the product is marketed.
The science and technology of verification has theoretical, experimental and production components. The basic mathematical logic of computational processes has advanced. There are new ways of specifying hardware and programs. Automatic theorem proving has advanced. There are large interactive theorem proving systems. In practical systems there have been advances in identifying the parts of a project for which formal methods are particularly needed.
The scientific community working on formal methods comprises mathematicians, logicians and computer scientists. Their number has increased, especially at Stanford and a few other places.

The Center for Formal Methods in computing comprises a group of Stanford Faculty, Research Associates and their industrial associates concerned with increasing the reliability of software and hardware by using mathematical methods of specifying and verifying them. Our focus individually and as a group is on the basic mathematical structure of computational processes, computer programs and reasoning systems.

Organizing Committee: Solomon Feferman, John McCarthy , John Mitchell, Vaughan Pratt and Carolyn Talcott. For now, questions should be adddressed to Pratt 723-2943, pratt@cs.stanford.edu.

The opportunity

Stanford University has outstanding faculty and research associates who have worked in various areas of the science and technology of formal methods of specification and verification of computational processes. We, the individuals listed below, are joining in the formation of the Center for Specification and Verification of Computational Processes to pursue both basic research and technological applications of formal methods. The work of the Center comprises long range basic research in formal specification and verification including computer-aided verification. [More sentences here]

The recent problems with the Pentium chip illustrate the importance of doing verification better and the need for more computer aided methods of verification. Here is a reference to the The Science, the Technology, the State of the Art, and Future Directions.

Stanford Faculty and Research Associates

The following faculty and research associates in the Computer Science, Mathematics, Philosophy and Electrical Engineering Departments are members of the Center. We expect to be joined by other faculty and by computer scientists in nearby companies.

Johan van Benthem (Center for the Study of Language and Information, Stanford & Institute for Logic, Language and Computation, Amsterdam) has worked in modal logic, temporal logic and logical analysis of natural languages (quantifiers, type structures). His current interest is dynamic logics of cognitive and physical action that span computer science, AI and linguistics. Specific themes in this line include: general theory of process equivalence, decidable dynamic versions of classical logics, proof theories for programming paradigms, heterogeneous information processing.

David Dill

Solomon Feferman is interested in the application of notions and methods from proof theory and constructive mathematics to the design and verification of functional programs. He has worked on logics of termination and correctness of such programs, and on abstract data types to encapsulate general procedures with both standard finitary types such as lists, trees, etc. as well as infinitary types such as streams and infinite precision reals. The latter work is in progress, and it appears that it is also of potential applicability to concurrent processes. He is Professor of Mathematics at Stanford, telephone 415 723-2439 , Email: sf@csli.stanford.edu.

Dr. Robert J. van Glabbeek works on aspects of concurrency theory, including branching time, true concurrency, and structured operational semantics.

Zohar Manna

John McCarthy has worked in the mathematical theory of proving that programs meet their specifications, in the design of programmming languages and in artificial intelligence. Recent work in connection with the programming language Elephant involves distinguishing between the input-output specifications and the accomplishment specifications of computer programs.

Grigori Mints is interested in the proof theory and its applications to program synthesis, complexity of algorithms, automated deduction and proof-checking. He applied strategies derived from proof theory to development of a wide spectrum of proof search programs both for classical logic and for new logics of computer science. He worked on connections with category theory that were later used for systems designed to model interaction, on deductive program synthesis as a basis of object-oriented systems, and on complete systems reflecting non-logical features of PROLOG.

John Mitchell works on foundational methods for programming language analysis and design, with particular emphasis on type systems that provide efficient tests for certain common programming errors. Recent work has led to new module systems, supporting modular, component-based program design, and type systems for object-oriented programming.

Prof. Vaughan Pratt works on duality theory and its applications to concurrency modeling, foundations of mathematics, and quantum mechanics.

Carolyn Talcott is interested in specification and reasoning about programs with facilities such as state and concurrency, and in open architectures for mechanized reasoning systems. She has recently developed theories, based on the Actor model, to treat interactions of components of open distributed computation systems. She currently participates in two formal reasoning projects: the FOL project, and the OMRS project. This work spans a broad range of experience in the design, analysis, and use of formalisms and of mechanized formal reasoning systems.

Associated Companies

Projects

The Concurrency Group conducts research on true concurrency with applications to design of parallel programming languages, semantics of distributed computing, and concurrency control in distributed databases.