Trustworthy Systems

Eisbach: A proof method language for isabelle

Authors

Daniel Matichuk, Toby Murray and Makarius Wenzel

NICTA\ UNSW

Abstract

Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance challenge. Isabelle’s most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means to write automated proof procedures. This can lead to more duplication in large proofs than is acceptable. In this paper we present Eisbach, a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to end-users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing some proof tools that are widely-used in the seL4 verification stack, and report on its strengths and limitations.

BibTeX Entry

  @article{Matichuk_MW_16,
    author           = {Matichuk, Daniel and Murray, Toby and Wenzel, Makarius},
    doi              = {10.1007/s10817-015-9360-2},
    journal          = {Journal of Automated Reasoning},
    keywords         = {isabelle, eisbach, proof automation, sel4, l4.verified},
    month            = mar,
    number           = {3},
    pages            = {261--282},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8465.pdf},
    title            = {Eisbach: A Proof Method Language for Isabelle},
    volume           = {56},
    year             = {2016}
  }

Download