Skip to main content

Proof Measurement and Estimation

Proof Measurement and Estimation

Proof Measurement and Estimation is an activity of the Trustworthy Systems project.

Graphs of Size of Statement vs Size of Proof, for two large subprojects of the seL4 verification.
  Graph of Size of Statement vs Size of Proof, for two large subprojects 
of the seL4 verification.
  Graph of Size of Proof vs Size of Statement, for two large subprojects 
of the seL4 verification.
  • Latest news:

  • Aims: understand how to measure and estimate large-scale formal verification projects by:

    • investigating measures for the size and complexity of formal verification artefacts (e.g. formal specifications, invariants, and proofs),
    • proposing models and approaches to estimate the size and effort required to complete formal verification projects,
    • empirically evaluating all of the above using NICTA's past and present formal verification projects.
  • Milestones:

  • Context:

    In traditional software engineering, development teams start with a requirements specification, design the system, implement it in a programming language, and then create and run test cases to check whether the system is built as designed and as required. However, because computer systems are so complex, testing can never check all possible behaviors of the system.

    Software engineering with formal methods is different. Teams start with a formal specification, which is a mathematical description of the requirements and/or design. Teams then use mathematical proof to show that the implemented system functions as designed and as required. This is called formal verification, and can provide an exhaustive check of all possible behaviors of the software. (Given some reasonable idealising assumptions about the underlying platform.)

    The formal verification projects undertaken at NICTA create large machine-checked mathematical proofs, authored by teams of people. However, running these large formal verification projects is a challenge. Estimating the size and effort of these projects is a key management challenge, but almost nothing is known about how to do this well.

  • Technical research challenges:

    • Are there better measures of the size of a formal verification proof than Lines of Proof?
    • Given a formal specification and a correct implementation, how big will the verification proof be?
    • As invariants are incrementally discovered during formal verification, what impact does that have on proof rework?
    • How much proof rework is caused by finding and fixing implementation bugs during formal verification?
    • After a formal verification project has started, how much longer will it take to finish?
  • Previous Events:

  • Publications:

    Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
    Empirical study towards a leading indicator for cost of formal software verification
    International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015
    Abstract PDF Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray
    An empirical research agenda for understanding formal methods productivity
    Information and Software Technology, Volume 60, pp. 102-112, January, 2015
    Abstract PDF Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski
    Productivity for proof engineering
    Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014
    Abstract PDF Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass
    Formal specifications better than function points for code sizing
    International Conference on Software Engineering, pp. 1257-1260, San Francisco, USA, May, 2013
    Abstract PDF June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu
    Large-scale formal verification in practice: A process perspective
    International Conference on Software Engineering, pp. 1002-1011, Zurich, Switzerland, June, 2012
    Abstract PDF Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski
    Simulation modeling of a large scale formal verification process
    International Conference on Software and Systems Process, pp. 3-12, Zurich, Switzerland, June, 2012

People

Past


Served by Apache on Linux on seL4.