Generalizing symbolic execution to library classes

13 years 10 months ago

Download users.ece.utexas.edu

Forward symbolic execution is a program analysis technique that allows using symbolic inputs to explore program executions. The traditional applications of this technique have focused on programs that manipulate primitive data types, such as integer or boolean. Recent extensions have shown how to handle reference types at their representation level. The extensions have favorably been backed by advances in constraint solving technology, and together they have made symbolic execution applicable, at least in theory, to a large class of programs. In practice, however, the increased potential for applications has created signiﬁcant issues with scalability of symbolic execution to programs of non-trivial size—the ensuing path conditions rapidly become unfeasibly complex. We present Dianju, a new technique that aims to address the scalability of symbolic execution. The fundamental idea in Dianju is to perform symbolic execution of commonly used library classes strings, sets and maps) at ...

Sarfraz Khurshid, Yuk Lai Suen

Real-time Traffic