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

In recent years there has been considerable interest in theories over stringequations, length function, and string-number conversion predicate within theformal verification, software engineering, and security communities. SMTsolvers for these theories, such as Z3str2, CVC4, and S3, are of immensepractical value in exposing security vulnerabilities in string-intensiveprograms. Additionally, there are many open decidability andcomplexity-theoretic questions in the context of theories over strings that areof great interest to mathematicians. Motivated by the above-mentionedapplications and open questions, we study a first-order, many-sorted,quantifier-free theory $T_{s,n}$ of string equations, linear arithmetic overstring length, and string-number conversion predicate and prove three theorems.First, we prove that the satisfiability problem for the theory $T_{s,n}$ isundecidable via a reduction from a theory of linear arithmetic over naturalnumbers with power predicate, we call power arithmetic. Second, we show thatthe string-numeric conversion predicate is expressible in terms of the powerpredicate, string equations, and length function. This second theorem, inconjunction with the reduction we propose for the undecidability theorem,suggests that the power predicate is expressible in terms of word equations andlength function if and only if the string-numeric conversion predicate is alsoexpressible in the same fragment. Such results are very useful tools incomparing the expressive power of different theories, and for establishingdecidability and complexity results. Third, we provide a consistentaxiomatization ${\Gamma}$ for the functions and predicates of $T_{s,n}$.Additionally, we prove that the theory $T_{\Gamma}$ , obtained via logicalclosure of ${\Gamma}$, is not a complete theory.

Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion