PROSPER was a 24 person-year ESPRIT Framework IV research project that investigated
software architectures for component-based, embedded formal verification tools. The aim of
the project was to make mechanized formal analysis more accessible in practice by providing
a framework for integrating formal proof tools inside other software applications.
This talk will discuss what we tried to achieve in the PROSPER project, sketch the
software toolkit we built, and describe our experience with some case studies. I will
then try to articulate some more general reflections about customised and embedded proof
support, arising from the PROSPER work and also my experience with another general
verification software framework -- the Forte system developed at Intel for industrial
microprocessor verification.
