PROSPER
The PROSPER toolkit. The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the PROSPER toolkit which enables this. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit.
Keywords for this software
References in zbMATH (referenced in 26 articles , 1 standard article )
Showing results 1 to 20 of 26.
Sorted by year (- Boulton, Richard; Hurd, Joe; Slind, Konrad: Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (2009)
- Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik: Integrating external deduction tools with ACL2 (2009)
- Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen: Verification of clock synchronization algorithms: experiments on a combination of deductive tools (2007)
- Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Providing a formal linkage between MDG and HOL (2007)
- Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen Fernanto: Verification of clock synchronization algorithms: Experiments on a combination of deductive tools. (2006)
- Grundy, Jim; Melham, Thomas F.; Krstic, Sava; Mclaughlin, Sean: Tool building requirements for an API to first-order solvers. (2006)
- Loer, Karsten; Harrison, Michael D.: An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation (2006)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
- Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula: Hidden verification for computational mathematics (2005)
- Mhamdi, Tarek; Tahar, Sofiène: Providing automated verification in HOL using MDGs (2004)
- Gordon, Mike; Hurd, Joe; Slind, Konrad: Executing the formal semantics of the Accellera property specification language by mechanised theorem proving (2003)
- Autexier, Serge; Mossakowski, Till: Integrating HOL-CASL into the development graph manager MAYA (2002)
- Celiku, Orieta; von Wright, Joakim: Theorem prover support for precondition and correctness calculation (2002)
- Gordon, Michael J.C.: PuzzleTool: An example of programming computation and deduction (2002)
- Melham, T.F.: PROSPER. An investigation into software architecture for embedded proof engines (2002)
- Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Formally linking MDG and HOL based on a verified MDG system (2002)
- Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
- Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula; Owre, Sam: Computer algebra meets automated theorem proving: Integrating Maple and PVS (2001)
- Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio: Communication protocols for mathematical services based on KQML and OMRS (2001)
- Armando, Alessandro; Zini, Daniele: Interfacing computer algebra and deduction systems via the logic broker architecture (2001)