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

Arguably the two most important techniques that are used in model checking to counter the combinatorial explosion in the number of states are abstraction and guidance. In this work we combine these techniques in a natural way by using (homomorphic) abstractions that reveal an error in the model to guide the model checker in searching for the error state in the original system. The mechanism used to achieve this is based on pattern databases, commonly used in artificial intelligence. A pattern database represents an abstraction and is used as a heuristic to guide the search. In essence, therefore, the same abstraction is used to reduce the size of the model and guide a search algorithm. We implement this approach in NuSMV and evaluate it using 2 well-known circuit benchmarks. The results show that this method can outperform the original model checker by several orders of magnitude, in both time and space.

Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases