The Tatami Project
Brief Summary of Results as of Sept. 2001

Formal methods increasingly play an important role in the development of reliable computer systems, but computer support for formal methods in general lags well behind the state of the art, and in particular, usually fails to take account of the situation today, in which most significant software and hardware systems are developed by large teams, usually distributed over space and time, using a combination of formal and informal methods and a variety of tools to attack different facets of the problem, while struggling with inadequate user interfaces, poor documentation, and difficult mathematics.

The Tatami project is designing, building and testing web-based tools to ameloriate these problems, by supporting distributed cooperative work using multiple logical systems and their integration, by paying careful attention to user interface design, and by having the tools generate web-based output that fully documents what was done, is easy to browse, and has links to tutorials on the underlying mathematics, as well as to informal explanations. The system is available over the internet, and is well documented and efficient.

Some particular innovations of this project include the following:

The Tatami project website is
It has had more than 8,000 hits in the last 3 years (not counting hits originating at UCSD). Many examples and papers produced by this project are linked from its homepage, including websites that have been produced by the Kumo system. The BOBJ proof engine also has a homepage,
which again has links to many examples, some of which may be rather surprising.

To the Tatami project homepage
Last modified: Wed Sep 26 21:09:20 PDT 2001