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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a novel approach for generalizing the IC3 algorithm for invariantchecking from finite-state to infinite-state transition systems, expressed oversome background theories. The procedure is based on a tight integration of IC3with Implicit (predicate) Abstraction, a technique that expresses abstracttran- sitions without computing explicitly the abstract system and isincremental with respect to the addition of predicates. In this scenario, IC3operates only at the Boolean level of the abstract state space, discoveringinductive clauses over the abstraction predicates. Theory reasoning is confinedwithin the underlying SMT solver, and applied transparently when performingsatisfiability checks. When the current abstraction allows for a spuriouscounterexample, it is refined by discov- ering and adding a sufficient set ofnew predicates. Importantly, this can be done in a completely incrementalmanner, without discarding the clauses found in the previous search. Theproposed approach has two key advantages. First, unlike current SMT gener-alizations of IC3, it allows to handle a wide range of background theorieswithout relying on ad-hoc extensions, such as quantifier elimination ortheory-specific clause generalization procedures, which might not always beavailable, and can moreover be inefficient. Second, compared to a directexploration of the concrete transition system, the use of abstraction gives asignificant performance improve- ment, as our experiments demonstrate.

IC3 Modulo Theories via Implicit Predicate Abstraction