English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Symbolic model checkers can construct proofs of properties over very complexmodels. However, the results reported by the tool when a proof succeeds do notgenerally provide much insight to the user. It is often useful for users tohave traceability information related to the proof: which portions of the modelwere necessary to construct it. This traceability information can be used todiagnose a variety of modeling problems such as overconstrained axioms andunderconstrained properties, and can also be used to measure completeness of aset of requirements over a model. In this paper, we present a new algorithm toefficiently compute the inductive validity core (IVC) within a model necessaryfor inductive proofs of safety properties for sequential systems. The algorithmis based on the UNSAT core support built into current SMT solvers and a novelencoding of the inductive problem to try to generate a minimal inductivevalidity core. We prove our algorithm is correct, and describe itsimplementation in the JKind model checker for Lustre models. We then present anexperiment in which we benchmark the algorithm in terms of speed, diversity ofproduced cores, and minimality, with promising results.

Efficient Generation of Inductive Validity Cores for Safety Properties