{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:38Z","timestamp":1774837838648,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642313738","type":"print"},{"value":"9783642313745","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_3","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"32-48","source":"Crossref","is-referenced-by-count":23,"title":["Challenges and Experiences in Managing Large-Scale Proofs"],"prefix":"10.1007","author":[{"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Daum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafal","family":"Kolanski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M., Leinenbach, D., Schirmer, N., Starostin, A.: The Verisoft Approach to Systems Verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 209\u2013224. Springer, Heidelberg (2008)"},{"issue":"2-4","key":"3_CR2","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s10817-009-9123-z","volume":"42","author":"E. Alkassar","year":"2009","unstructured":"Alkassar, E., Hillebrand, M., Leinenbach, D., Schirmer, N., Starostin, A., Tsyban, A.: Balancing the load \u2014 leveraging a semantics stack for systems verification. JAR: Special Issue Operat. Syst. Verification\u00a042(2-4), 389\u2013454 (2009)","journal-title":"JAR: Special Issue Operat. Syst. Verification"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Appel, K., Haken, W.: Every map is four colourable. Bulletin of the American Mathematical Society, 711\u2013712 (1976)","DOI":"10.1090\/S0002-9904-1976-14122-5"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"3_CR7","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem (2005), \n                    \n                      http:\/\/research.microsoft.com\/en-us\/people\/gonthier\/4colproof.pdf"},{"issue":"11","key":"3_CR8","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof \u2014 the four-color theorem. Notices of the American Mathematical Society\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"3_CR10","volume-title":"The Pragmatic Programmer: From Journeyman to Master","author":"A. Hunt","year":"2000","unstructured":"Hunt, A., Thomas, D.: The Pragmatic Programmer: From Journeyman to Master. Addison-Wesley, Reading (2000)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: 22nd SOSP, Big Sky, MT, USA, pp. 207\u2013220. ACM (October 2009)","DOI":"10.1145\/1629575.1629596"},{"key":"3_CR12","unstructured":"Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs (2012), \n                    \n                      http:\/\/afp.sf.net"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) 33rd POPL, Charleston, SC, USA, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"3_CR14","series-title":"LNCS","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"3_CR15","first-page":"311","volume-title":"Workshop on Types for Proofs and Programs","author":"P. Rudnicki","year":"1992","unstructured":"Rudnicki, P.: An overview of the MIZAR project. In: Workshop on Types for Proofs and Programs, pp. 311\u2013332. Chalmers University of Technology, Bastad (1992)"},{"key":"3_CR16","unstructured":"Ruegenberg, M.: Semi-automatic proof refactoring for Isabelle. Undergraduate thesis, Technische Universit\u00e4t M\u00fcnchen (2011)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"3_CR19","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M. Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as Document-Oriented Proof Assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol.\u00a06824, pp. 244\u2013259. Springer, Heidelberg (2011)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-22673-1_18","volume-title":"Intelligent Computer Mathematics","author":"I. Whiteside","year":"2011","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards Formal Proof Script Refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol.\u00a06824, pp. 260\u2013275. Springer, Heidelberg (2011)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-03359-9_34","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Winwood","year":"2009","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the Gap: A Verification Framework for Low-Level. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 500\u2013515. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:30:06Z","timestamp":1556890206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}