Zero false positive code analysis in Java with dynamic symbolic execution

This talk is going to show how dynamic symbolic execution technique can be used to search deep bugs in Java without false positives. We will classify code analysis kinds and show contemporary techniques for these tasks. Symbolic execution implementation details in Java will be revealed — you'll be able to write your own analyzer. We'll review state-of-art in this area. Additionally, you will learn simple interface for solving NP-hard problems in your Java application — SMT solver. We will encode well known NP-complete problems (like Sudoku) in SMT on Java using most popular solver - Microsoft Z3.

This talk is inspired by last year's DotNext talk.