Keynote Talk : Scaling Z3 in Azure

Nikolaj Bjorner
Microsoft Research Redmond (USA)


Nikolaj Bjørner is a Principal Researcher at Microsoft Research. He received his Ph.D. in Computer Science from Stanford University in 1998 and then worked at Kestrel Institute on techniques for program synthesis, transformation and specification. He then developed distributed file systems at XDegrees and Microsoft’s core file systems group where he designed the DFSR, Distributed File System Replication, shipped with Windows Server since 2005. Nikolaj is currently at Microsoft Research and works on the theorem prover, Z3. It is used in various program analysis and verification tools, used among other places, in Microsoft Security Risk Detection system and static driver verifier tools, and SecGuru which powers security checking of all firewall configurations in Microsoft Azure. In 2014, the tool paper that introduced Z3 was awarded the most influential tool paper for the first 20 years of TACAS and in 2015 Z3 received the ACM SIGPLAN systems award.


Z3 is an efficient satisfiability modulo theories solver. It is widely used for program analysis, verification and testing, and selectively in other areas, such as product configuration and scheduling. We describe uses of Z3 and associated architectures in cloud based services, where depending on the application, response times are expected in milli-seconds or acceptable within hours, but not days or years. To verify network configurations in Azure, Z3 runs in a service that checks thousands of router configurations every day. The checks take milliseconds and provide immediate feedback to network changes. In the opposite end of the spectrum, for hard combinatorial constraints, we extended Z3 with a cube and conquer solver to run as a distributed service.



Dates (New)

February 04, 2018

Abstract submission deadline

February 11, 2018

Paper submission deadline

March 26, 2018

Acceptance notification

April 04, 2018

Camera ready copy due



The proceedings of the conference will be published in Springer’s Lecture Notes in Computer Science

Partners & Sponsors (Pending)