Article ID Journal Published Year Pages File Type
421585 Electronic Notes in Theoretical Computer Science 2012 5 Pages PDF
Abstract

We describe the Proverʼs Palette, a general, modular architecture for combining tools for formal verification, with the key differentiator that the integration emphasises the role of the user. A concrete implementation combining the theorem prover Isabelle with the computer algebra systems Maple and QEPCAD-B is then presented. This illustrates that the design principles of the Proverʼs Palette simplify tool integrations while enhancing the power and usability of theorem provers.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics