Trustworthy Systems

Productivity for proof engineering

Authors

Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski

NICTA

UNSW

Purdue University

Abstract

Recent projects such as L4.verified (the verification of the seL4 microkernel) have demonstrated that large-scale formal program verification is now becoming practical. Such projects introduce a new kind of artifact into the software engineering process: proofs. ‘Proof engineering’ is the creation and maintenance of proofs, and is supported by tools and techniques to manage their size and complexity. In this paper we address an important but unstudied aspect of proof engineering: proof productivity. We have extracted size and effort data from the history of the development of nine projects associated with L4.verified. We find strong linear relationships between effort (in person-weeks) and size (in lines of proof script) for projects and for individuals. We discuss opportunities and limitations with the use of lines of proof as a size measure for examining proof productivity, and discuss the importance of understanding proof productivity for future research on effort estimation models and productivity improvement in proof engineering.

BibTeX Entry

  @inproceedings{Staples_JAMKK_14,
    address          = {Turin, Italy},
    author           = {Staples, Mark and Jeffery, Ross and Andronick, June and Murray, Toby and Klein, Gerwin and Kolanski,
                        Rafal},
    booktitle        = {Empirical Software Engineering and Measurement},
    keywords         = {proof engineering, productivity, proof sizing, formal verification},
    month            = sep,
    pages            = {15},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8105.pdf},
    title            = {Productivity for Proof Engineering},
    year             = {2014}
  }

Download