Online Enumeration of All Minimal Inductive Validity Cores

D 2018

Online Enumeration of All Minimal Inductive Validity Cores

BENDÍK, Jaroslav, Elaheh GHASSABANI, Michael WHALEN a Ivana ČERNÁ

Základní údaje

Originální název

Online Enumeration of All Minimal Inductive Validity Cores

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant, domácí), Elaheh GHASSABANI (840 Spojené státy), Michael WHALEN (840 Spojené státy) a Ivana ČERNÁ (203 Česká republika, domácí)

Vydání

LNCS 10886. Neuveden, Software Engineering and Formal Methods - 16th International Conference, od s. 189-204, 16 s. 2018

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00101018

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-92969-9

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-92970-5_12

UT WoS

000445248600012

Klíčová slova anglicky

Inductive Validity Cores;SMT-based model checking;Inductive proofs;Traceability;Proof cores

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 30. 4. 2019 08:14, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

MUNI/A/0854/2017, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BENDÍK, Jaroslav, Elaheh GHASSABANI, Michael WHALEN a Ivana ČERNÁ. Online Enumeration of All Minimal Inductive Validity Cores. In Einar Broch Johnsen and Ina Schaefer. Software Engineering and Formal Methods - 16th International Conference. LNCS 10886. Neuveden: Springer International Publishing, 2018, s. 189-204. ISBN 978-3-319-92969-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-92970-5_12.

@inproceedings{1421699,
   author = {Bendík, Jaroslav and Ghassabani, Elaheh and Whalen, Michael and Černá, Ivana},
   address = {Neuveden},
   booktitle = {Software Engineering and Formal Methods - 16th International Conference},
   doi = {http://dx.doi.org/10.1007/978-3-319-92970-5_12},
   edition = {LNCS 10886},
   editor = {Einar Broch Johnsen and Ina Schaefer},
   keywords = {Inductive Validity Cores;SMT-based model checking;Inductive proofs;Traceability;Proof cores},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-92969-9},
   pages = {189-204},
   publisher = {Springer International Publishing},
   title = {Online Enumeration of All Minimal Inductive Validity Cores},
   year = {2018}
}

TY  - JOUR
ID  - 1421699
AU  - Bendík, Jaroslav - Ghassabani, Elaheh - Whalen, Michael - Černá, Ivana
PY  - 2018
TI  - Online Enumeration of All Minimal Inductive Validity Cores
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319929699
KW  - Inductive Validity Cores;SMT-based model checking;Inductive proofs;Traceability;Proof cores
N2  - 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.
ER  -

BENDÍK, Jaroslav, Elaheh GHASSABANI, Michael WHALEN a Ivana ČERNÁ. Online Enumeration of All Minimal Inductive Validity Cores. In Einar Broch Johnsen and Ina Schaefer. \textit{Software Engineering and Formal Methods - 16th International Conference}. LNCS 10886. Neuveden: Springer International Publishing, 2018, s.~189-204. ISBN~978-3-319-92969-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-92970-5\_{}12.

Podrobný výpis o publikaci