Verification of String Programs via Automata

string solving, automaton, model checking, formal verification

Modern implementations of web servers are densely interlaced with string manipulations and their control flow depends heavily on values of string variables.The cost of a software bug is rapidly raising, which yields the need of investigation on new techniques for static analysis of string programs. Recently, string solving-reasoning about constraints over string variables-has shown a great potential to facilitate automated reasoning about such programs (finding bugs, test generation, automatic repair, etc.). Despite the theoretical undecidability of string solving, the works from Holík et al. (2017) and Scott and Sherman (2014) have shown the potential of methods based on finite automata in deciding practical subclasses of the problem. Our work focuses on improving performance of model checking of finite automata, scaling the applications of automata-based string solving while also contributing to other fields of formal verification and synthesis that benefit from the automata theory.