An Evaluation of Automata Algorithms for String Analysis

Abstract. There has been significant recent interest in automated rea-soning techniques, in particular constraint solvers, for string variables. These techniques support a wide range of clients, ranging from static analysis to automated testing. The majority of string constraint solvers rely on finite automata to support regular expression constraints. For these approaches, performance depends critically on fast automata oper-ations such as intersection, complementation, and determinization. Ex-isting work in this area has not yet provided conclusive results as to which core algorithms and data structures work best in practice. In this paper, we study a comprehensive set of algorithms and data structures for performing fast automata operations. Our goal is to pro-vide an apples-to-apples comparison between techniques that are used in current tools. To achieve this, we re-implemented a number of existing techniques. We use an established set of regular expressions benchmarks as an indicative workload. We also include several techniques that, to the best of our knowledge, have not yet been used for string constraint solv-ing. Our results show that there is a substantial performance difference across techniques, which has implications for future tool design.