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

We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

Efficient SAT-based unbounded symbolic model checking using circuit cofactoring