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

The use of interpolants in model checking is becoming an enabling technologyto allow fast and robust verification of hardware and software. The applicationof encodings based on the theory of arrays, however, is limited by theimpossibility of deriving quantifier- free interpolants in general. In thispaper, we show that it is possible to obtain quantifier-free interpolants for aSkolemized version of the extensional theory of arrays. We prove this in twoways: (1) non-constructively, by using the model theoretic notion ofamalgamation, which is known to be equivalent to admit quantifier-freeinterpolation for universal theories; and (2) constructively, by designing aninterpolating procedure, based on solving equations between array updates.(Interestingly, rewriting techniques are used in the key steps of the solverand its proof of correctness.) To the best of our knowledge, this is the firstsuccessful attempt of computing quantifier- free interpolants for a variant ofthe theory of arrays with extensionality.

Quantifier-Free Interpolation of a Theory of Arrays