Online enumeration of all minimal inductive validity cores

Jaroslav Bendík, Elaheh Ghassabani, Michael Whalen, Ivana Černá

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

2 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. Minimal Inductive Validity Cores (MIVCs) trace a property to a minimal set of model elements necessary for constructing a proof, and can help to explain why a property is true of a model. In addition, the traceability information provided by MIVCs can be used to perform a variety of engineering analysis such as coverage analysis, robustness analysis, and vacuity detection. The more MIVCs are identified, the more precisely such analyses can be performed. Nevertheless, a full enumeration of all MIVCs is in general intractable due to the large number of possible model element sets. The bottleneck of existing algorithms is that they are not guaranteed to emit minimal IVCs until the end of the computation, so returned results are not known to be minimal until all solutions are produced. In this paper, we propose an algorithm that identifies MIVCs in an online manner (i.e., one by one) and can be terminated at any time. We benchmark our new algorithm against existing algorithms on a variety of examples, and demonstrate that our algorithm not only is better in intractable cases but also completes the enumeration of MIVCs faster than competing algorithms in many tractable cases.

Original languageEnglish (US)
Title of host publicationSoftware Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Proceedings
EditorsEinar Broch Johnsen, Ina Schaefer
PublisherSpringer- Verlag
Pages189-204
Number of pages16
ISBN (Print)9783319929699
DOIs
StatePublished - Jan 1 2018
Event16th International Conference on Software Engineering and Formal Methods, SEFM 2018 Held as Part of STAF 2018 - Toulouse, France
Duration: Jun 27 2018Jun 29 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10886 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Conference on Software Engineering and Formal Methods, SEFM 2018 Held as Part of STAF 2018
CountryFrance
CityToulouse
Period6/27/186/29/18

Keywords

  • Inductive proofs
  • Inductive validity cores
  • Proof cores
  • SMT-based model checking
  • Traceability

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

  • Cite this

    Bendík, J., Ghassabani, E., Whalen, M., & Černá, I. (2018). Online enumeration of all minimal inductive validity cores. In E. B. Johnsen, & I. Schaefer (Eds.), Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Proceedings (pp. 189-204). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10886 LNCS). Springer- Verlag. https://doi.org/10.1007/978-3-319-92970-5_12