Trustworthy Systems

An Isabelle proof method language

Authors

Daniel Matichuk, Makarius Wenzel and Toby Murray

NICTA

UNSW

Univ. Paris-Sud
France

CNRS

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 desirable. In this paper we present a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to existing users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing some tactics widely-used in the seL4 verification stack, and report on its strengths and limitations.

BibTeX Entry

  @inproceedings{Matichuk_WM_14,
    address          = {Vienna, Austria},
    author           = {Matichuk, Daniel and Wenzel, Makarius and Murray, Toby},
    booktitle        = {International Conference on Interactive Theorem Proving},
    doi              = {10.1007/978-3-319-08970-6_25},
    editor           = {{Gerwin Klein and Ruben Gamboa}},
    keywords         = {proof automation, proof procedure language, isabelle},
    month            = jul,
    pages            = {390--405},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7847.pdf},
    publisher        = {Springer},
    title            = {An {Isabelle} Proof Method Language},
    year             = {2014}
  }

Download