Title: The Satisfiability Modulo Theories solver Z3 Speaker: Nikolaj Bjorner (http://research.microsoft.com/en-us/people/nbjorner/)   Abstract: Automated reasoning has become an integral part of software engineering tools in recent years thanks to high-performance theorem provers. The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, Pex, Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Spec Explorer, SecGuru, and Terminator. These tools reduce program analysis, verification and testing problems to logic queries that are solved using Z3. The talk takes these applications of Z3 as a starting point and examines applications SAGE, Dafny and SecGuru in some more depth. SAGE uses dynamic symbolic execution. It has been used to eradicate hundreds of security vulnerabilities in media readers that are otherwise well-known to be prone to security critical bugs. Dafny is a program verification environment and presents the current state-of-the-art in program verification methodologies and tools. SecGuru is a tool for automatically validating network connectivity restriction policies in large scale data-centers such as Windows Azure. We then describe some of the current trends in Z3: including solving recursive Horn clauses, solving real and floating point arithmetic.   

Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.