Edinburgh Research Explorer

Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
Pages (from-to)115-119
Number of pages5
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2012


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.

    Research areas

  • Maple

Download statistics

No data available

ID: 5725026