Proof-based coverage metrics for formal verification

Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Heimdahl, Lucas Wagner

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

6 Scopus citations

Abstract

When using formal verification on critical software, an important question involves whether we have we specified enough properties for a given implementation model. To address this question, coverage metrics for property-based formal verification have been proposed. Existing metrics are usually based on mutation, where the implementation model is repeatedly modified and re-analyzed to determine whether mutant models are 'killed' by the property set. These metrics tend to be very expensive to compute, as they involve many additional verification problems. This paper proposes an alternate family of metrics that can be computed using the recently introduced idea of Inductive Validity Cores (IVCs). IVCs determine a minimal set of model elements necessary to establish a proof. One of the proposed metrics is both rigorous and substantially cheaper to compute than mutation-based metrics. In addition, unlike the mutation-based techniques, the design elements marked as necessary by the metric are guaranteed to preserve provability. We demonstrate the metrics on a large corpus of examples.

Original languageEnglish (US)
Title of host publicationASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
EditorsTien N. Nguyen, Grigore Rosu, Massimiliano Di Penta
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages194-199
Number of pages6
ISBN (Electronic)9781538626849
DOIs
StatePublished - Nov 20 2017
Event32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 - Urbana-Champaign, United States
Duration: Oct 30 2017Nov 3 2017

Publication series

NameASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering

Other

Other32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017
CountryUnited States
CityUrbana-Champaign
Period10/30/1711/3/17

Keywords

  • Coverage
  • formal verification
  • inductive proofs
  • inductive validity cores
  • requirements completeness

Fingerprint Dive into the research topics of 'Proof-based coverage metrics for formal verification'. Together they form a unique fingerprint.

Cite this