ASE 2017

2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017), October 30 – November 3, 2017, Urbana-Champaign, IL, USA

Desktop Layout

Formal Verification
Technical Research
Proof-Based Coverage Metrics for Formal Verification
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats P. E. Heimdahl, and Lucas Wagner
(University of Minnesota, USA; Rockwell Collins, USA)
Supplementary Material
Abstract: When using formal verification on critical software, an important question involves whether the properties used for analysis are sufficient to adequately constrain the behavior of an 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.


Time stamp: 2019-09-22T01:24:46+02:00