Abstract / Description of output
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 language | English |
---|---|
Title of host publication | Fundamental Approaches to Software Engineering |
Subtitle of host publication | 19th 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 |
Publisher | Springer |
Pages | 325-341 |
Number of pages | 17 |
ISBN (Electronic) | 978-3-662-49665-7 |
ISBN (Print) | 978-3-662-49664-0 |
DOIs | |
Publication status | Published - Mar 2016 |
Event | 19th International Conference of Fundamental Approaches to Software Engineering - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016 https://www.etaps.org/index.php/2016 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Berlin Heidelberg |
Volume | 9633 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 19th International Conference of Fundamental Approaches to Software Engineering |
---|---|
Abbreviated title | FASE 2016 |
Country/Territory | Netherlands |
City | Eindhoven |
Period | 2/04/16 → 8/04/16 |
Internet address |
Fingerprint
Dive into the research topics of 'Towards Formal Proof Metrics'. Together they form a unique fingerprint.Profiles
-
David Aspinall
- School of Informatics - Personal Chair in Software Safety and Security
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active