PROSPER - An Investigation into Software Architecture for Embedded Proof Engines

摘要: PROSPER is a recently-completed ESPRIT Framework IV research project that investigated software architectures for component-based, embedded formal verification tools. The aim of the was to make mechanized analysis more accessible in practice by providing framework integrating proof tools inside other applications. This paper an extended abstract invited presentation on Prosper given at FroCoS 2002. It describes vision and provides summary technical approach taken some lessons learned.