11 citations · 24 across the 5 of their papers we have counts for
4 papers · 1 filter
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
Murphy Berzish, Mitja Kulczynski, Federico Mora +4
We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement…
Z3str3: A String Solver with Theory-aware Branching
Murphy Berzish, Yunhui Zheng, Vijay Ganesh
We present a new string SMT solver, Z3str3, that is faster than its competitors Z3str2, Norn, CVC4, S3, and S3P over a majority of three industrial-strength benchmarks, namely Kalu…
A Solver for a Theory of Strings and Bit-vectors
Sanu Subramanian, Murphy Berzish, Yunhui Zheng +2
We present a solver for a many-sorted first-order quantifier-free theory of string equations, string length represented as bit-vectors, and bit-vector arithmetic aimed a…
Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion
Vijay Ganesh, Murphy Berzish
In recent years there has been considerable interest in theories over string equations, length function, and string-number conversion predicate within the formal verification, soft…