Trustworthy Systems

Challenges and experiences in managing large-scale proofs

Authors

Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski

NICTA

UNSW

Abstract

Large-scale verification projects pose particular challenges. Issues include proof exploration, efficiency of the edit-check cycle, and proof refactoring for documentation and maintainability. We draw on insights from two large-scale verification projects, L4.verified and Verisoft, that both used the Isabelle/HOL prover. We identify the main challenges in large-scale proofs, propose possible solutions, and discuss the Levity tool, which we developed to automatically move lemmas to appropriate theories, as an example of the kind of tool required by such proofs.

BibTeX Entry

  @inproceedings{Bourke_DKK_12,
    address          = {Bremen, Germany},
    author           = {Bourke, Timothy and Daum, Matthias and Klein, Gerwin and Kolanski, Rafal},
    booktitle        = {Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management},
    editor           = {{Makarius Wenzel}},
    keywords         = {large-scale proofs, isabelle/hol, interactive theorem proving},
    month            = jul,
    pages            = {32--48},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5717.pdf},
    publisher        = {Springer},
    title            = {Challenges and Experiences in Managing Large-Scale Proofs},
    year             = {2012}
  }

Download