Paper Info
Title
PROSPER - An Investigation into Software Architecture for Embedded Proof Engines
Abstract
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 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 paper is an extended abstract of an invited presentation on Prosper given at FroCoS 2002. It describes the vision of the Prosper project and provides a summary of the technical approach taken and some of the lessons learned.
Year
DOI
Venue
2002
10.1007/3-540-45988-X_16
FroCos
Keywords
Field
DocType
formal proof tool,prosper project,research project,technical approach,software application,software architecture,embedded formal verification tool,recently-completed esprit framework iv,mechanized formal analysis,proof engines,formal verification
Software tool,Model checking,Software engineering,Computer science,Software,Application programming interface,Software architecture,Operating system,Distributed computing,Formal proof,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-43381-3
0
0.34
References 
Authors
26
1
Name
Order
Citations
PageRank
Thomas F. Melham138435.63