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

This paper investigates the combination of abstract interpretation over thedomain of convex polyhedra with interpolant tree automata, in anabstraction-refinement scheme for Horn clause verification. These techniqueshave been previously applied separately, but are combined in a new way in thispaper. The role of an interpolant tree automaton is to provide a generalisationof a spurious counterexample during refinement, capturing a possibly infiniteset of spurious counterexample traces. In our approach these traces are theneliminated using a transformation of the Horn clauses. We compare this approachwith two other methods; one of them uses interpolant tree automata in analgorithm for trace abstraction and refinement, while the other uses abstractinterpretation over the domain of convex polyhedra without the generalisationstep. Evaluation of the results of experiments on a number of Horn clauseverification problems indicates that the combination of interpolant treeautomaton with abstract interpretation gives some increase in the power of theverification tool, while sometimes incurring a performance overhead.

Interpolant Tree Automata and their Application in Horn Clause Verification