Symbolic string execution

[摘要] ENGLISH ABSTRACT: Symbolic execution is a well-established technique for automated test generationand fornding errors in complex code. Most of the focus has howeverbeen on programs that manipulate integers, booleans, and even, references inobject-oriented programs. Recently researchers have started looking at programsthat do lots of string processing, motivated, in part, by the popularity ofthe web and the risk that errors in web servers may lead to security violations.Attempts to extend symbolic execution to the domain of strings are mainlydivided into one of two camps: automata-based approaches and approachesbased on bitvector analysis. Here we investigate these two approaches in auni ed setting, namely the symbolic execution framework of Java PathFinder.We describe the implementations of both approaches and then do an evaluationto show under what circumstances each approach performs well (or notso well). We also illustrate the usefulness of the symbolic execution of stringsbynding errors in real-world examples.

[发布机构] Stellenbosch University