Efficient generation of all minimal inductive validity cores

Elaheh Ghassabani, Michael Whalen, Andrew Gacek

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

9 Scopus citations

Abstract

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Recently, proof cores (alternately, for inductive model checkers, Inductive Validity Cores (IVCs)) were introduced to trace a property to a minimal set of model elements necessary for proof. Minimal IVCs facilitate several engineering tasks, including performing traceability and analyzing requirements completeness, that usually rely on the minimality of IVCs. However, existing algorithms for generating an IVC are either expensive or only able to find an approximately minimal IVC. Besides minimality, computing all minimal IVCs of a given property is an interesting problem that provides several useful analyses, including regression analysis for testing/proof, determination of the minimum (as opposed to minimal) number of model elements necessary for proof, the diversity examination of model elements leading to proof, and analyzing fault tolerance. This paper proposes an efficient method for finding all minimal IVCs of a given property proving its correctness and completeness. We benchmark our algorithm against existing IVC-generating algorithms and show, in many cases, the cost of finding all minimal IVCs by our technique is similar to finding a single minimal IVC using existing algorithms.

Original languageEnglish (US)
Title of host publicationProceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017
EditorsGeorg Weissenbacher, Daryl Stewart
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages31-38
Number of pages8
ISBN (Electronic)9780983567875
DOIs
StatePublished - Nov 8 2017
Event17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 - Vienna, Austria
Duration: Oct 2 2017Oct 6 2017

Publication series

NameProceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017

Conference

Conference17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017
CountryAustria
CityVienna
Period10/2/1710/6/17

Keywords

  • Inductive proofs
  • Inductive Validity Cores
  • SMT-based model checking
  • UNSAT-core generation

Fingerprint Dive into the research topics of 'Efficient generation of all minimal inductive validity cores'. Together they form a unique fingerprint.

Cite this