Challenges and experiences in managing large-scale proofs

Timothy Bourke; Matthias Daum; Gerwin Klein; Rafal Kolanski

doi:10.1007/978-3-642-31374-5_3

Challenges and experiences in managing large-scale proofs

Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings
Pages	32-48
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-642-31374-5_3
Publication status	Published - 17 Aug 2012
Externally published	Yes
Event	Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 - Bremen, Germany Duration: 8 Jul 2012 → 13 Jul 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7362 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012
Country/Territory	Germany
City	Bremen
Period	8/07/12 → 13/07/12

Keywords

Interactive theorem proving
Isabelle/HOL
Large-scale proof

Access to Document

10.1007/978-3-642-31374-5_3

Cite this

Bourke, T., Daum, M., Klein, G., & Kolanski, R. (2012). Challenges and experiences in managing large-scale proofs. In Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings (pp. 32-48). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7362 LNAI). https://doi.org/10.1007/978-3-642-31374-5_3

Bourke, Timothy ; Daum, Matthias ; Klein, Gerwin et al. / Challenges and experiences in managing large-scale proofs. Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings. 2012. pp. 32-48 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e1586df4a66a4bb08fb55e637f07a5ab,

title = "Challenges and experiences in managing large-scale proofs",

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.",

keywords = "Interactive theorem proving, Isabelle/HOL, Large-scale proof",

author = "Timothy Bourke and Matthias Daum and Gerwin Klein and Rafal Kolanski",

year = "2012",

month = aug,

day = "17",

doi = "10.1007/978-3-642-31374-5\_3",

language = "English",

isbn = "9783642313738",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "32--48",

booktitle = "Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings",

note = "Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 ; Conference date: 08-07-2012 Through 13-07-2012",

}

Bourke, T, Daum, M, Klein, G & Kolanski, R 2012, Challenges and experiences in managing large-scale proofs. in Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7362 LNAI, pp. 32-48, Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012, Bremen, Germany, 8/07/12. https://doi.org/10.1007/978-3-642-31374-5_3

Challenges and experiences in managing large-scale proofs. / Bourke, Timothy; Daum, Matthias; Klein, Gerwin et al.
Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings. 2012. p. 32-48 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7362 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Challenges and experiences in managing large-scale proofs

AU - Bourke, Timothy

AU - Daum, Matthias

AU - Klein, Gerwin

AU - Kolanski, Rafal

PY - 2012/8/17

Y1 - 2012/8/17

N2 - 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.

AB - 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.

KW - Interactive theorem proving

KW - Isabelle/HOL

KW - Large-scale proof

U2 - 10.1007/978-3-642-31374-5_3

DO - 10.1007/978-3-642-31374-5_3

M3 - Conference contribution

AN - SCOPUS:84864929103

SN - 9783642313738

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 32

EP - 48

BT - Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings

T2 - Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012

Y2 - 8 July 2012 through 13 July 2012

ER -

Bourke T, Daum M, Klein G, Kolanski R. Challenges and experiences in managing large-scale proofs. In Intelligent Computer Mathematics - 11th Int. Conf., AISC 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, DML 2012, 11th Int. Conf., MKM 2012, Systems and Projects, Part of CICM 2012, Proceedings. 2012. p. 32-48. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-31374-5_3

Challenges and experiences in managing large-scale proofs

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this