2016/05/30 by Ganesh, Vijay, Berzish, Murphy
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1605.09442
In recent years there has been considerable interest in theories over string equations, length function, and string-number conversion predicate within the formal verification, software engineering, and security communities. SMT solvers for these theories, such as Z3str2, CVC4, and S3, are of immense practical value in exposing security vulnerabilities in string-intensive programs. Additionally, there are many open decidability and complexity-theoretic questions in the context of theories over strings that are of great interest to mathematicians. Motivated by the above-mentioned applications and open questions, we study a first-order, many-sorted, quantifier-free theory Ts,n of string equations, linear arithmetic over string length, and string-number conversion predicate and prove three theorems. First, we prove that the satisfiability problem for the theory Ts,n is undecidable via a reduction from a theory of linear arithmetic over natural numbers with power predicate, we call power arithmetic. Second, we show that the string-numeric conversion predicate is expressible in terms of the power predicate, string equations, and length function. This second theorem, in conjunction with the reduction we propose for the undecidability theorem, suggests that the power predicate is expressible in terms of word equations and length function if and only if the string-numeric conversion predicate is also expressible in the same fragment. Such results are very useful tools in comparing the expressive power of different theories, and for establishing decidability and complexity results. Third, we provide a consistent axiomatization Γ for the functions and predicates of Ts,n. Additionally, we prove that the theory TΓ , obtained via logical closure of Γ, is not a complete theory.