Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
421585 | Electronic Notes in Theoretical Computer Science | 2012 | 5 Pages |
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