Symbolic execution in .NET: Automated tests generation, verification, and program synthesis

This talk is about the not-so-distant future when a lot of testing and verification work will be done automatically. But some practical advice and things that "can be used right now" will be presented also. Symbolic execution is a powerful technique for program analysis and test generation that has become popular in recent years. We'll dive into the theory behind Microsoft IntelliTest, understand how you can use symbolic execution for your purposes. Open source Symbolic Virtual VM V# will be explained with examples and an introduction.

Another practical skill after this lecture is the application of SMT-solver: we will encode different hobby tasks like Sudoku, Minesweeper into SMT restrictions and ask the solver to solve them for us. In the end, we will speak about the possible Next Big Thing that will change the development paradigm — Program Synthesis.