The PROSPER Toolkit

Louise A. Dennis; Graham Collins; Michael Norrish; Richard Boulton; Konrad Slind; Graham Robinson; Mike Gordon; Tom Melham

doi:10.1007/3-540-46419-0_7

The PROSPER Toolkit

Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, Tom Melham

Formal Methods

Research output: Other contribution › peer-review

Abstract

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.

Original language	Undefined
Publisher	Springer Nature
Number of pages	15
ISBN (Print)	9783540672821
ISBN (Electronic)	9783540464198
DOIs	https://doi.org/10.1007/3-540-46419-0_7
Publication status	Published - 2000

Publication series

Name	Lecture Notes in Computer Science
Volume	1785

Keywords

Model checker
Decision procedure
Propositional logic
Theorem prove
Proof obligation

Access to Document

10.1007/3-540-46419-0_7

Cite this

@misc{84014f8c364549b0beec4cda37225e02,

title = "The PROSPER Toolkit",

abstract = "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 = "Model checker, Decision procedure, Propositional logic, Theorem prove, Proof obligation",

author = "Dennis, {Louise A.} and Graham Collins and Michael Norrish and Richard Boulton and Konrad Slind and Graham Robinson and Mike Gordon and Tom Melham",

year = "2000",

doi = "10.1007/3-540-46419-0_7",

language = "Undefined",

isbn = "9783540672821",

series = " Lecture Notes in Computer Science",

publisher = "Springer Nature",

address = "United States",

type = "Other",

}

TY - GEN

T1 - The PROSPER Toolkit

AU - Dennis, Louise A.

AU - Collins, Graham

AU - Norrish, Michael

AU - Boulton, Richard

AU - Slind, Konrad

AU - Robinson, Graham

AU - Gordon, Mike

AU - Melham, Tom

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

KW - Model checker

KW - Decision procedure

KW - Propositional logic

KW - Theorem prove

KW - Proof obligation

U2 - 10.1007/3-540-46419-0_7

DO - 10.1007/3-540-46419-0_7

M3 - Other contribution

SN - 9783540672821

T3 - Lecture Notes in Computer Science

PB - Springer Nature

ER -