One of the major aims of the PROSPER project is to make formal specification and verification techniques more user-friendly. At Edinburgh, the Language Technology Group is contributing to this goal by developing novel interfaces for requirements capture:

1. Natural language input for specifying hardware properties. The idea is to allow the expression of temporal logic constraints on circuits though sentences of a restricted subset of English. We have an experimental convertor available, which is exploited by our online demonstration of model checking with English specifications.
2. A graphically enhanced interface tool. We are now developing an extension of our natural language work which introduces graphical representations of signal traces - waveforms - in order to significantly improve the usability of the tool.

These interfaces will be exploited in PROSPER through the construction of prototype tools in collaboration with our industrial partners. In addition, the open architecture being developed for PROSPER components will allow these interfaces to be used in a variety of other applications.

While not a formal PROSPER partner, Edinburgh's Mathematical Reasoning Group constitutes a significant resource for the overall project effort, having particular expertise in the integration of the HOL theorem prover with other systems.