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

Constrained Horn Clauses (CHCs) are often used in automated programverification. Thus, techniques for (dis-)proving satisfiability of CHCs are avery active field of research. On the other hand, acceleration techniques forcomputing formulas that characterize the N-fold closure of loops havesuccessfully been used for static program analysis. We show how to useacceleration to avoid repeated derivations with recursive CHCs in resolutionproofs, which reduces the length of the proofs drastically. This idea givesrise to a novel calculus for (dis)proving satisfiability of CHCs, calledAcceleration Driven Clause Learning (ADCL). We implemented this new calculus inour tool LoAT and evaluate it empirically in comparison to otherstate-of-the-art tools.

ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses