One of our intentions is to keep an up to date list of non-traditional applications of formal methods that we are aware of. The following list serves this purpose by listing applications according to the following topics:

- Science
- Humanities and Social Sciences
- Creative Arts and Entertainment
- Official Documents, Procedures and Manuals

- Although, Peter Wegner's ideas on the relationship between interaction and physics (see for example this paper) do not use a formal method directly, the spirit of Wegner's work is strongly influenced by concurrency theory.

- Chris Tofts work on analysing ant behaviour with probabilistic process algebra, see the publications on this page.

- There is work on modelling the user with formal methods, see for example, the projects Programmable User Modelling Applications and TACIT,
- John Rushby et al's work in the formal methods and dependable systems group at SRI on analysing cockpit interfaces using model checking and theorem proving. See for example this paper, this paper and this paper.

- Work by David Duce, David Duke, Phil Barnard, Jon May et al on syndetic modelling (see, for example, the publications under the title "Mathematical Models of Cognitive Processing" on this page).
- Work by Howard Bowman and Giorgio Faconti on modelling the Interactive Cogntive Subsystems architecture using LOTOS, see this page.
- Work by Ann Blandford et al on cognitive modelling using logical and set theoretic notations, see the PUMA project.
- Paul Curzon's recent work on HOL based usability analysis (see this page).
- There has even been a Z specification of the
Soar Architecture -
B. Milnes "A Specification of the Soar Cognitive Architecture in Z" Technical Report CMU-CSS-92-169, Carnegie Mellon University, 1992.

- Paul Hudak has worked on music composition using functional languages (which although not formal methods are close enough for this entry to be made) and game theory, see this paper.

- Chris Johnson et al's work in the Glasgow Accident Analysis Group on describing and analysing accident reports using formal methods. See, for example, this page, this paper or this paper.
- Peter Wright et al's work on using Petri Nets to describe accident scenarios, see for example, this paper and other papers on this page. In particular, Michael Harrison has been involved in a number of related applications of formal methods.
- Peter Ladkin et al's work on describing user manuals using the temporal logic of actions. See, for example, the WB-Analysis home page, this paper or this paper.
- Harold Thimbleby has also done a great deal of work on formal interpretation of user manuals, e.g. the following papers, 0, 1, 2, 3, 4, 5.
- Graziella Tonfoni's work on eliminating fuzziness and mis-interpretation in written communication, see for example this page and this (microsoft word) document.

Last modified December 1999.

Contact Howard Bowman if you have
problems or comments.