Invited talk
SMT in Verification, Modeling, and Testing at Microsoft
Dr. Nikolaj Bjorner (Microsoft Research)
The Satisfiability Modulo Theories (SMT) solver, Z3, from Microsoft Research is a state-of-the art theorem prover that integrates specialized solvers for domains that are of relevance for program analysis, testing and verification. Z3 has been used within and outside of Microsoft for the past few years including the Windows 7 static driver verifier, the SAGE white-box fuzzer for finding security vulnerabilities, Pex, in a Verifying C Compiler, the Verve verified operating system and the Dafny verified program environment. This talk delves into some of the more recent efforts around Z3, in particular using Z3 in a firewall analysis engine, and adventures in using Z3 for points-to analysis in JavaScript malware detection, and finally emerging support for reachability queries by solving Satisfiability Modulo Theories for Horn clauses.
Speaker Bio
Nikolaj is a Senior Researcher at Microsoft Research working in the area of Automated Theorem Proving and Software Engineering. Nikolaj's current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of many software engineering tools, including test-case generation, smart fuzzing, static analysis, program verification, software model checking, model-based software design and synthesis. Previously, Nikolaj designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at XDegrees (a startup acquired by Microsoft), and program synthesis and transformation systems at the research company Kestrel Institute. Nikolaj received my Master's and Ph.D. degrees in computer science from Stanford University.
Keynote speakers
As in previous years, the post-conference proceedings will be published in Springer's Lecture Notes in Computer Science series (LNCS).
HVC 2012 Poster
