Proof and Specification Assisted
Design Environments

ESPRIT Framework IV LTR 26241

PROSPER is a collaboration involving the University of Glasgow (UK), the University of Cambridge (UK), the University of Edinburgh (UK), the Universities of Karlsruhe and Tübingen (D), IFAD (DK), and Prover Technology (S). The University of Glasgow acts as the project coordinator. The project is developing an extensible, open proof tool architecture for incorporating formal verification into industrial CAD/CASE tool flows and design methodologies. The tools include novel user-friendly interfaces, and will be tested on two major example systems.

Site Index
Project Summary
Some presentations on PROSPER

A glossary and summary for the Toolkit
- The PROSPER Toolkit
- PROSPER plugins (verification components)
Natural Language Interface work at Edinburgh
Papers, reports and other documents
Selected public deliverables
Mailing lists
Announcements and discussions related to PROSPER
Support for PROSPER software
Related projects, conferences and other links
Registered Users
Login to project partners' area.

University of Glasgow, UK (Tom Melham)
University of Cambridge, UK (Mike Gordon)
University of Edinburgh, UK (Ewan Klein)
Universität Tübingen, Germany (Thomas Kropf)
Prover Technology AB, Sweden (Lars Lundgren)
IFAD, Denmark (Kim Sunesen)
Full list of participants

Contact Point
Prof. T. F. Melham
Department of Computing Science
University of Glasgow
Glasgow, Scotland, G12 8QQ

Tel: +44 141 330 4967
Fax: +44 141 330 4913

Page maintained by Richard Boulton.
Please e-mail any comments or suggestions to