Nikolaj Bjørner and Leonardo de Moura are Researchers in the Research in Software Engineering (RiSE) team at Microsoft Research. They are talking and demoing Z3, a high-performance SMT constraint solver. Solving constraint systems is the root of of many software analysis techniques so it is not surprising to see Z3 powering many tools developed at Microsoft: Spec#/Boogie, Pex, SLAM, SAGE, FORMULA, HAVOC and more.
In this video, you'll get a 10000 feet overview of Z3 and constraint solving in general with a demo on how to use the C# API. For more details, you will find many articles that should keep you busy for a while.
The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.