Efficient symbolic execution of strings for validating web applications
Daryl Shannon, Indradeep Ghosh, S. Rajan, Sarfraz Khurshid · 2009
Symbolic execution is a popular technique used in formal verification of software and hardware systems. In this paper we examine three different ways of performing symbolic execution for the purpose of formal model checking, on web application software implemented with the Java programming language. We evaluate the different techniques on real industrial applications and compare them on issues of performance, implementation ease, and ease-of-use. There are some special characteristics of web applications like extensive use of string inputs that need to be tackled before traditional symbolic execution techniques become feasible. We provide details of how we have solved those issues.