Abstract: Bug-finding tools that are based on approximate analysis often report false positives. Burned enough by false positives, a skeptical programmer wants to see convincing evidence that a bug report is indeed feasible. Symbolic analysis can often help produce such evidence in the form of a concrete test case that can reproduce a feasible bug. In this talk, I will describe recent work my colleagues and I have done on symbolic analysis of Java programs. In much of the talk, I will focus on the technology needed to make symbolic analysis work effectively on real-world Java applications, without requiring hand-written specifications of procedures, and without inlining procedure calls away. I will report on our experience with building a bug report validator based on symbolic analysis, and discuss some open research questions. I will also demonstrate additional applications of our symbolic analysis engine.