@inproceedings { , title = {System Description: Embedding Verification into Microsoft Excel}, abstract = {The aim of the PROSPER project is to allow the embedding of existing verification technology into applications in such a way that the theorem proving is hidden, or presented to the end user in a natural way. This paper describes a system built to test whether the PROSPER toolkit satisfied this aim. The system combines the toolkit with Microsoft Excel, a popular commercial spreadsheet application.}, conference = {Automted Deduction (CADE-17)}, organization = {Pennsylvania}, publicationstatus = {Published}, url = {https://nottingham-repository.worktribe.com/output/1023639}, year = {2000}, author = {Collins, Graham and Dennis, Louise Abigail} editor = {McAllester, David} }