Paper Info
Title
Online Enumeration of All Minimal Inductive Validity Cores.
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.
Year
DOI
Venue
2018
10.1007/978-3-319-92970-5_12
Lecture Notes in Computer Science
Keywords
Field
DocType
Inductive validity cores,SMT-based model checking,Inductive proofs,Traceability,Proof cores
Bottleneck,Computer science,Enumeration,Engineering analysis,Real-time computing,Robustness (computer science),Theoretical computer science,Mathematical proof,Traceability,Computation
Conference
Volume
ISSN
Citations 
10886
0302-9743
0
PageRank 
References 
Authors
0.34
11
4
Name
Order
Citations
PageRank
Jaroslav Bendík162.82
Elaheh Ghassabani2182.72
Michael W. Whalen3109670.54
Ivana Cerná425017.48