skip to main content
10.1145/2652524.2652551acmconferencesArticle/Chapter ViewAbstractPublication PagesesemConference Proceedingsconference-collections
research-article

Productivity for proof engineering

Published: 18 September 2014 Publication History

Abstract

Context: Recent projects such as L4.verified (the verification of the seL4 microkernel) have demonstrated that large-scale formal program verification is now becoming practical.
Objective: We address an important but unstudied aspect of proof engineering: proof productivity.
Method: We extracted size and effort data from the history of the development of nine projects associated with L4.verified.
Results: We find strong linear relationships between effort and proof size for projects and for individuals. We discuss opportunities and limitations with the use of lines of proof as a size measure, and discuss the importance of understanding proof productivity for future research.
Conclusions: An understanding of proof productivity will assist in its further industrial application and provide a basis for cost estimation and understanding of rework and tool usage.

References

[1]
Aitken, J. S., Gray, P., Melham, T., and Thomas, M. 1998. Interactive theorem proving: an empirical study of user activity, Journal of Symbolic Computation, vol. 25 (2).
[2]
Andronick, J., Jeffery, R., Klein, G., Kolanski, R., Staples, M., Zhang, H., and Zhu, L. 2012. Large-scale formal verification in practice: a process perspective. ICSE 2012. 1002--1011.
[3]
Curzon, P. 1995. The importance of proof maintenance and reengineering. Int. Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track, 17--32.
[4]
Kaivola, R. and Kohatsu, K. 2003. Proof engineering in the large: formal verification of Pentium4 floating-point divider. Int J Softw Tools Technol Transfer, vol. 4 (3), 323--334.
[5]
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., and Heiser, G. Comprehensive formal verification of an OS microkernel. ACM Trans. Comp. Sys. Vol. 32 (1), 2:1--2:70.
[6]
Nipkow, T., Paulson, L., and Wenzel, M. 2002. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic. LNCS vol. 2283.
[7]
Runeson, P. and Höst, M. 2008. Guidelines for conducting and reporting case study research in software engineering, Empirical Software Engineering, vol. 14 (2), 131--164.
[8]
Staples, M., Kolanski, R., Klein, G., Lewis, C., Andronick, J., Murray, T., Jeffery, R., and Bass, L. 2013. Formal specifications better than function points for code sizing. ICSE 2013. 1257--1260.
[9]
Syme, D. 1998. Interaction for declarative theorem proving. Available from http://research.microsoft.com
[10]
Trendowicz, A. and Jeffery, R. 2014. Software project effort estimation: Foundations and best practice guidelines for success, Springer.
[11]
Trendowicz, A. and Münch, J. 2009. Factors influencing software development productivity -- State of the art and industrial experiences, Advances in Computers, vol. 77.
[12]
Wenzel, M. M. 2001. Isabelle/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München.
[13]
Wright, H. K., Kim, M., and Perry, D. E. 2010. Validity concerns in software engineering research, Proc. of FoSER 2010, 411--414.

Cited By

View all
  • (2024)Code to Qed, the Project Manager's Guide to Proof EngineeringACM Transactions on Software Engineering and Methodology10.1145/366480733:7(1-50)Online publication date: 26-Aug-2024
  • (2021)Verified secure compilation for mixed-sensitivity concurrent programsJournal of Functional Programming10.1017/S095679682100016231Online publication date: 28-Jul-2021
  • (2020)REPLica: REPL instrumentation for Coq analysisProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373823(99-113)Online publication date: 20-Jan-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ESEM '14: Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement
September 2014
461 pages
ISBN:9781450327749
DOI:10.1145/2652524
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 September 2014

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. formal verification
  2. productivity
  3. proof engineering
  4. proof sizing

Qualifiers

  • Research-article

Funding Sources

Conference

ESEM '14
Sponsor:

Acceptance Rates

ESEM '14 Paper Acceptance Rate 23 of 123 submissions, 19%;
Overall Acceptance Rate 130 of 594 submissions, 22%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)11
  • Downloads (Last 6 weeks)1
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Code to Qed, the Project Manager's Guide to Proof EngineeringACM Transactions on Software Engineering and Methodology10.1145/366480733:7(1-50)Online publication date: 26-Aug-2024
  • (2021)Verified secure compilation for mixed-sensitivity concurrent programsJournal of Functional Programming10.1017/S095679682100016231Online publication date: 28-Jul-2021
  • (2020)REPLica: REPL instrumentation for Coq analysisProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373823(99-113)Online publication date: 20-Jan-2020
  • (2017)Provably trustworthy systemsPhilosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences10.1098/rsta.2015.0404375:2104(20150404)Online publication date: 4-Sep-2017
  • (2015)Empirical study towards a leading indicator for cost of formal software verificationProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818842(722-732)Online publication date: 16-May-2015
  • (2015)A product line of theories for reasoning about safe evolution of product linesProceedings of the 19th International Conference on Software Product Line10.1145/2791060.2791105(161-170)Online publication date: 20-Jul-2015
  • (2015)Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification2015 IEEE/ACM 37th IEEE International Conference on Software Engineering10.1109/ICSE.2015.85(722-732)Online publication date: May-2015
  • (2015)Mining the Archive of Formal ProofsProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_1(3-17)Online publication date: 13-Jul-2015

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media