Computing Mutation Coverage in Interpolation-Based Model Checking

Hana Chockler; Daniel Kroening; Mitra Purandare

doi:10.1109/TCAD.2011.2180382

Computing Mutation Coverage in Interpolation-Based Model Checking

Hana Chockler^*, Daniel Kroening, Mitra Purandare

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

5 Citations (Scopus)

Abstract

Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This reuse permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the model checker.

Original language	English
Pages (from-to)	765-778
Number of pages	14
Journal	Ieee transactions on computer-Aided design of integrated circuits and systems
Volume	31
Issue number	5
DOIs	https://doi.org/10.1109/TCAD.2011.2180382
Publication status	Published - May 2012

Keywords

Coverage
interpolation
model checking
DESIGN-INTENT COVERAGE
FORMAL VERIFICATION
LOWER BOUNDS
METRICS
GENERATION

Access to Document

10.1109/TCAD.2011.2180382

Cite this

@article{ea4564b27d624a7e8c6eb2edbf367d00,

title = "Computing Mutation Coverage in Interpolation-Based Model Checking",

abstract = "Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This reuse permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the model checker.",

keywords = "Coverage, interpolation, model checking, DESIGN-INTENT COVERAGE, FORMAL VERIFICATION, LOWER BOUNDS, METRICS, GENERATION",

author = "Hana Chockler and Daniel Kroening and Mitra Purandare",

year = "2012",

month = may,

doi = "10.1109/TCAD.2011.2180382",

language = "English",

volume = "31",

pages = "765--778",

journal = "Ieee transactions on computer-Aided design of integrated circuits and systems",

issn = "0278-0070",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "5",

}

TY - JOUR

T1 - Computing Mutation Coverage in Interpolation-Based Model Checking

AU - Chockler, Hana

AU - Kroening, Daniel

AU - Purandare, Mitra

PY - 2012/5

Y1 - 2012/5

N2 - Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This reuse permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the model checker.

AB - Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This reuse permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the model checker.

KW - Coverage

KW - interpolation

KW - model checking

KW - DESIGN-INTENT COVERAGE

KW - FORMAL VERIFICATION

KW - LOWER BOUNDS

KW - METRICS

KW - GENERATION

U2 - 10.1109/TCAD.2011.2180382

DO - 10.1109/TCAD.2011.2180382

M3 - Article

SN - 0278-0070

VL - 31

SP - 765

EP - 778

JO - Ieee transactions on computer-Aided design of integrated circuits and systems

JF - Ieee transactions on computer-Aided design of integrated circuits and systems

IS - 5

ER -

Computing Mutation Coverage in Interpolation-Based Model Checking

Abstract

Keywords

Access to Document

Fingerprint

Cite this