For many problems arising in the setting of graph querying (such as finding semantic associations RDF graphs, exact and approximate pattern matching, sequence alignment, etc.), power standard languages such widely studied conjunctive regular path queries (CRPQs) is insufficient at least two ways. First, they cannot output paths second, more crucially, express relationships among paths. We thus propose a class extended CRPQs, called ECRPQs, which add relations on tuples paths, allow variables...

The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, with such applications as symbolic execution strings automated detection cross-site scripting (XSS) vulnerabilities web applications. A (symbolic) given a finite sequence assignments assertions (i.e. without loops), its amounts to determining the existence inputs that yield successful execution. Modern programming languages (e.g. JavaScript, PHP, Python)...

We study the fundamental issue of decidability satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type operations yields decidability, little is known about their combined theory, which especially relevant when analysing security vulnerabilities dynamic web pages in a more realistic browser model. On hand, word equations (string logic concatenations) cannot precisely capture sanitisation functions (e.g....

String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection cross-site scripting, and test-case generation. A popular string technique includes symbolic executions, which at their core use constraint solvers over domain, a.k.a. solvers. Such typically reason constraints expressed in theories with concatenation operator as an atomic constraint. In recent years, researchers started to recognise...

The theory of strings with concatenation has been widely argued as the basis constraint solving for verifying string-manipulating programs. However, this is far from adequate expressing many string constraints that are also needed in practice; example, use regular (pattern matching against a expression), and string-replace function (replacing either first occurrence or all occurrences ``pattern'' constant/variable/regular expression by ``replacement'' constant/variable), among others. Both...

Regular expressions are a classical concept in formal language theory. programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), well additional features capturing groups and references. While symbolic execution programs containing RegExes appeals to string solvers natively supporting important RegEx, solver is hitherto missing. In this paper, we propose the first theory that provides support. The key idea our introduce new...

We revisit the classic problem of proving safety over parameterised concurrent systems, i.e., an infinite family finite-state systems that are represented by some finite (symbolic) means. An example such is a dining philosopher protocol with any number n processes (n being parameter defines family). Regular model checking well-known generic framework for modelling where set configurations (resp. transitions) regular transducer). Although verifying properties in undecidable general, many...

Theories over strings are among the most heavily researched logical theories in SMT community past decade, owing to error-prone nature of string manipulations, which often leads security vulnerabilities (e.g. cross-site scripting and code injection). The majority existing decision procedures solvers for these themselves intricate; they complicated algorithmically, also have deal with a very rich vocabulary operations. This has led plethora bugs implementation, instance been discovered...

Parikh’s Theorem is a fundamental result in automata theory with numerous applications computer science. These include software verification (e.g. infinite-state verification, string constraints, and of arrays), cryptographic protocols using Horn clauses modulo equational theories) database querying evaluating path-queries graph databases), among others. states that the letter-counting abstraction language recognized by finite or context-free grammars definable Linear Integer Arithmetic...

We study the fundamental issue of decidability satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type operations yields decidability, little is known about their combined theory, which especially relevant when analysing security vulnerabilities dynamic web pages in a more realistic browser model. On hand, word equations (string logic concatenations) cannot precisely capture sanitisation functions (e.g....

HTML5 applications normally have a large set of CSS (Cascading Style Sheets) rules for data display. Each rule consists node selector and declaration block (which assigns values to selected nodes' display attributes). As web evolve, maintaining files can easily become problematic. Some will be replaced by new ones, but these obsolete (hence redundant) often remain in the applications. Not only does this "bloat" – increasing bandwidth requirement it also significantly increases browsers'...

We study the problem of computing transitive closure tree-automatic (binary) relations, which are represented by tree automata. Such relations include classes infinite systems generated pushdown (PDS), ground rewrite (GTRS), PA-processes, and Turing machines, to name a few. Although this is unsolvable in general, we provide semi-algorithm for prove completeness guarantee PDS, GTRS, PA-processes. The an extension known structure-preserving guaranteed several interesting parameterized over...

Verifying safety and liveness over array systems is a highly challenging problem. Array naturally capture parameterized such as distributed protocols with an unbounded number of processes. Such often exploit process IDs during their computation, resulting in whose element values range infinite domain. In this paper, we develop novel framework for proving systems. The crux the to overapproximate system string rewriting (i.e. finite alphabet) by means new predicate abstraction that exploits...

We study Satisfiability Modulo Theories (SMT) enriched with the so-called Ramsey quantifiers, which assert existence of cliques (complete graphs) in graph induced by some formulas. The extended framework is known to have applications proving program termination (in particular, whether a transitive binary predicate well-founded), and monadic decomposability SMT Our main result new algorithm for eliminating quantifiers from three common theories: Linear Integer Arithmetic (LIA), Real (LRA),...

Ground tree rewrite systems (GTRS) are an extension of pushdown with the ability to spawn new sub threads that hierarchically structured. In this paper, we study following problems over GTRS:(1) model checking EF-logic, (2)weak bi similarity against finite systems, and (3) strong systems. Although they all known be decidable, show (1) (2) have nonelementbisimilarityy, whereasproblem is shown in coNEXP by finding a syntactic fragment EFwhose complexity complete for P <sup...