Towards Formal Proof Metrics

David Aspinall, Cezary Kaliszyk

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Recent years have seen increasing success in building large formal proof developments using interactive theorem provers (ITPs). Some proofs have involved many authors, years of effort, and resulted in large, complex interdependent sets of proof “source code” files. Developing these in the first place, and maintaining and extending them afterwards, is a considerable challenge. It has prompted the idea of Proof Engineering as a new sub-field, to find methods and tools to help. It is natural to try to borrow ideas from Software Engineering for this. In this paper we investigate the idea of defining proof metrics by analogy with software metrics. We seek metrics that may help to monitor and compare formal proof developments, which might be used to guide good practice, locate likely problem areas, or suggest refactorings. Starting from metrics that have been proposed for object-oriented design, we define analogues for formal proofs. We show that our metrics enjoy reasonable properties, and we demonstrate their behaviour with some practical experiments, showing changes over time as proof developments evolve, and making comparisons across different ITPs.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering
Subtitle of host publication19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages17
ISBN (Electronic)978-3-662-49665-7
ISBN (Print)978-3-662-49664-0
Publication statusPublished - Mar 2016
Event19th International Conference of Fundamental Approaches to Software Engineering - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference19th International Conference of Fundamental Approaches to Software Engineering
Abbreviated titleFASE 2016
Internet address


Dive into the research topics of 'Towards Formal Proof Metrics'. Together they form a unique fingerprint.

Cite this