Challenges and Experiences in Managing Large-Scale Proofs

Select |




Print


Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal


2012-07-09


Conference Material


Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management


Bremen, Germany


32-48


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.


Springer


Large-scale proofs, Isabelle/HOL, Interactive theorem proving


http://www.informatik.uni-bremen.de/cicm2012/cicm.php?event=mkm&menu=general


The final publication is available at www.springerlink.com


nicta:5717


Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal. Challenges and Experiences in Managing Large-Scale Proofs. In: Makarius Wenzel Editor, editor/s. Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management; Bremen, Germany. Springer; 2012-07-09. 32-48.http://hdl.handle.net/102.100.100/100137?index=1



Loading citation data...

Citation counts
(Requires subscription to view)