System Description: Embedding Verification into Microsoft Excel

Collins, Graham; Dennis, Louise Abigail

doi:10.1007/10721959_40

All Outputs (8)

A poetry performance in a collaborative virtual environment (2000)
Journal Article
Benford, S., Reynard, G., Greenhalgh, C., Snowdon, D., & Bullock, A. (2000). A poetry performance in a collaborative virtual environment. IEEE Computer Graphics and Applications, 20(3), https://doi.org/10.1109/38.844374

'Exploiting problem structure in a genetic algorithm approach to a nurse rostering problem' (2000)
Journal Article
Aickelin, U., & Dowsland, K. (2000). 'Exploiting problem structure in a genetic algorithm approach to a nurse rostering problem'

There is considerable interest in the use of genetic algorithms to solve problems arising in the areas of scheduling and timetabling. However, the classical genetic algorithm paradigm is not well equipped to handle the conflict between objectives and... Read More about 'Exploiting problem structure in a genetic algorithm approach to a nurse rostering problem'.

Structured cases in case-based reasoning: re-using and adapting cases for time-tabling problems (2000)
Journal Article
Burke, E., MacCarthy, B. L., Petrovic, S., & Qu, R. (2000). Structured cases in case-based reasoning: re-using and adapting cases for time-tabling problems. Knowledge-Based Systems, 13(2-3),

In this paper, we present a case-based reasoning (CBR) approach solving educational time-tabling problems. Following the basic idea behind CBR, the solutions of previously solved problems are employed to aid finding the solutions for new problems. A... Read More about Structured cases in case-based reasoning: re-using and adapting cases for time-tabling problems.

The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction (2000)
Journal Article
Dennis, L. A., Bundy, A., & Green, I. (2000). The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction. Annals of Mathematics and Artificial Intelligence, 29(1-4),

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coi... Read More about The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction.

The PROSPER Toolkit (2000)
Presentation / Conference Contribution
Dennis, L. A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., …Melham, T. (2000). The PROSPER Toolkit. In S. Graf, & M. Schwartzbach (Eds.),

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 incorporatin... Read More about The PROSPER Toolkit.

The Development of an On-line Submission and Peer Review System (2000)
Presentation / Conference Contribution
Pavey, P., Probets, S., & Brailsford, D. F. (2000). The Development of an On-line Submission and Peer Review System. In P. Linde, J. Smith, & E. Emelianova (Eds.),

Online submission and peer review is emerging as the next step forward for many journal publishers in an ever increasing drive to take advantage of technological improvements in transferring data electronically over the internet. The Electronic Submi... Read More about The Development of an On-line Submission and Peer Review System.

Integrating SVC and HOL with the PROSPER Toolkit (2000)
Presentation / Conference Contribution
Stevenson, A., & Dennis, L. A. (2000). Integrating SVC and HOL with the PROSPER Toolkit.

We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit.
The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL... Read More about Integrating SVC and HOL with the PROSPER Toolkit.

System Description: Embedding Verification into Microsoft Excel (2000)
Presentation / Conference Contribution
Collins, G., & Dennis, L. A. System Description: Embedding Verification into Microsoft Excel. Presented at Automted Deduction (CADE-17)

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 te... Read More about System Description: Embedding Verification into Microsoft Excel.