{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:44Z","timestamp":1774837964441,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496640","type":"print"},{"value":"9783662496657","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_19","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"325-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Towards Formal Proof Metrics"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31374-5_1","volume-title":"Intelligent Computer Mathematics","author":"J Alama","year":"2012","unstructured":"Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for coq and mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 1\u201316. Springer, Heidelberg (2012)"},{"issue":"2","key":"19_CR2","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/2089116.2089118","volume":"21","author":"J Al-Dallal","year":"2012","unstructured":"Al-Dallal, J., Briand, L.C.: A precise method-method interaction-based cohesion metric for object-oriented classes. ACM Trans. Softw. Eng. Methodol. 21(2), 8:1\u20138:34 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"3\u20134","key":"19_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1021966832558","volume":"29","author":"G Bancerek","year":"2002","unstructured":"Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in MIZAR. J. Autom. Reasoning 29(3\u20134), 189\u2013224 (2002)","journal-title":"J. Autom. Reasoning"},{"issue":"10","key":"19_CR4","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1109\/32.544352","volume":"22","author":"VR Basili","year":"1996","unstructured":"Basili, V.R., Briand, L.C., Melo, W.L.: A validation of object-oriented design metrics as quality indicators. IEEE Trans. Softw. Eng. 22(10), 751\u2013761 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-20615-8_1","volume-title":"Intelligent Computer Mathematics","author":"JC Blanchette","year":"2015","unstructured":"Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 3\u201317. Springer, Heidelberg (2015)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Intelligent Computer Mathematics","author":"T Bourke","year":"2012","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 32\u201348. Springer, Heidelberg (2012)"},{"issue":"6","key":"19_CR7","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1109\/32.295895","volume":"20","author":"SR Chidamber","year":"1994","unstructured":"Chidamber, S.R., Kemerer, C.F.: A metrics suite for object oriented design. IEEE Trans. Softw. Eng. 20(6), 476\u2013493 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR8","unstructured":"Demeyer, S., Ducasse, S.: Metrics, do they really help? In: Malenfant, J. (ed.) Proceedings LMO 1999 (Languages et Models a Objets), pp. 69\u201382 (1999)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Demeyer, S., Ducasse, S., Nierstrasz, O.: Finding refactorings via change metrics. In: Object-Oriented Programming Systems, Languages & Applications, OOPSLA 2000, pp. 166\u2013177 (2000)","DOI":"10.1145\/354222.353183"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Mathematics, E.: The odd order theorem proof. In: Principles of Programming Languages, POPL 2013, pp. 1\u20132. ACM (2013)","DOI":"10.1145\/2480359.2429071"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013)"},{"issue":"10","key":"19_CR12","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"TC Hales","year":"2007","unstructured":"Hales, T.C.: The jordan curve theorem, formally and informally. Am. Math. Mon. 114(10), 882\u2013894 (2007)","journal-title":"Am. Math. Mon."},{"key":"19_CR13","unstructured":"Hales, T.C., et al.: A formal proof of the Kepler conjecture. In: CoRR abs\/1501.02155 (2015)"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","volume":"44","author":"TC Hales","year":"2010","unstructured":"Hales, T.C., et al.: A revision of the proof of the kepler conjecture. Discrete Comput. Geom. 44(1), 1\u201334 (2010)","journal-title":"Discrete Comput. Geom."},{"issue":"2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reasoning 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011)"},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.infsof.2014.11.005","volume":"60","author":"RD Jeffery","year":"2015","unstructured":"Jeffery, R.D., et al.: An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. 60, 102\u2013112 (2015)","journal-title":"Inf. Softw. Technol."},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reasoning 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-06410-9_2","volume-title":"FM 2014: Formal Methods","author":"G Klein","year":"2014","unstructured":"Klein, G.: Proof engineering considered essential. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 16\u201321. Springer, Heidelberg (2014)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: Formal verification of an OS kernel. In: Symposium on Operating Systems Principles SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: Machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Marcus, A., Poshyvanyk, D.: The conceptual cohesion of classes. In: IEEE International Conference on Software Maintenance, ICSM 2005, pp. 133\u2013142 (2005)","DOI":"10.1109\/ICSM.2005.89"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Matichuk, D., et al.: Empirical study towards a leading indicator for cost of formal software verification. In: International Conference on Software Engineering, ICSE 2015, pp. 722\u2013732 (2015)","DOI":"10.1109\/ICSE.2015.85"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/978-3-319-08434-3_27","volume-title":"Intelligent Computer Mathematics","author":"K P\u0105k","year":"2014","unstructured":"P\u0105k, K.: Automated improving of proof legibility in the mizar system. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 373\u2013387. Springer, Heidelberg (2014)"},{"issue":"1\u20132","key":"19_CR25","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1\u20132), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: User Interfaces for Theorem Provers (UITP) (1998)","DOI":"10.1006\/jsco.1997.0171"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Simon, F., Steinbruckner, F., Lewerentz, C.: Metrics based refactoring. In: Software Maintenance and Reengineering, CSMR. 2001, pp. 30\u201338 (2001)","DOI":"10.1109\/CSMR.2001.914965"},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world \u2013 Infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 1\u201312. Springer, Heidelberg (2010)"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/978-3-319-08434-3_27","volume-title":"Intelligent Computer Mathematics","author":"K P\u0105k","year":"2014","unstructured":"P\u0105k, K.: Automated improving of proof legibility in the mizar system. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 373\u2013387. Springer, Heidelberg (2014)"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-75560-9_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Urban","year":"2007","unstructured":"Urban, J., Sutcliffe, G.: ATP cross-verification of the mizar MPTP challenge problems. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 546\u2013560. Springer, Heidelberg (2007)"},{"issue":"9","key":"19_CR31","doi-asserted-by":"publisher","first-page":"1357","DOI":"10.1109\/32.6178","volume":"14","author":"EJ Weyuker","year":"1988","unstructured":"Weyuker, E.J.: Evaluating software complexity measures. IEEE Trans. Software Eng. 14(9), 1357\u20131365 (1988)","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:29:22Z","timestamp":1748813362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}