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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

String analysis is the problem of reasoning about how strings are manipulatedby a program. It has numerous applications including automatic detection ofcross-site scripting (XSS). A popular string analysis technique includessymbolic executions, which at their core use string (constraint) solvers. Suchsolvers typically reason about constraints expressed in theories over stringswith the concatenation operator as an atomic constraint. In recent years,researchers started to recognise the importance of incorporating thereplace-all operator and finite transductions in the theories of strings withconcatenation. Such string operations are typically crucial for reasoning aboutXSS vulnerabilities in web applications, especially for modelling sanitisationfunctions and implicit browser transductions (e.g. innerHTML).  In this paper, we provide the first string solver that can reason aboutconstraints involving both concatenation and finite transductions. Moreover, ithas a completeness and termination guarantee for several important fragments(e.g. straight-line fragment). The main challenge addressed in the paper is theprohibitive worst-case complexity of the theory. To this end, we propose amethod that exploits succinct alternating finite automata as concise symbolicrepresentations of string constraints. Alternation offers not only exponentialsavings in space when representing Boolean combinations of transducers, butalso a possibility of succinct representation of otherwise costly combinationsof transducers and concatenation. Reasoning about the emptiness of the AFAlanguage requires a state-space exploration in an exponential-sized graph, forwhich we use model checking algorithms (e.g. IC3). We have implemented ouralgorithm and demonstrated its efficacy on benchmarks that are derived from XSSand other examples in the literature.

String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)