Towards Formal Proof Metrics

David Aspinall, Cezary Kaliszyk

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

Abstract

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
Pages325-341
Number of pages17
ISBN (Electronic)978-3-662-49665-7
ISBN (Print)978-3-662-49664-0
DOIs
Publication statusPublished - Mar 2016
Event19th International Conference of Fundamental Approaches to Software Engineering - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
https://www.etaps.org/index.php/2016

Publication series

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

Conference

Conference19th International Conference of Fundamental Approaches to Software Engineering
Abbreviated titleFASE 2016
Country/TerritoryNetherlands
CityEindhoven
Period2/04/168/04/16
Internet address

Fingerprint

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

Cite this