Powering Z3 using Azure and empowering Azure with Z3Published: Tuesday, 04 December 2018
Speaker: Nikolaj Bjorner, Microsoft Research Time: 13:00 on Friday 7th December Location: Kilburn 1.4 Title: Powering Z3 using Azure and empowering Azure with Z3.
Speaker: Nikolaj Bjorner, Microsoft Research
Time: 13:00 on Friday 7th December
Location: Kilburn 1.4
Title: Powering Z3 using Azure and empowering Azure with Z3.
We describe synergies between symbolic solving and cloud infrastructures.
In one direction, verification methods have important uses in running a reliable and secure cloud.
Conversely, scalable cloud infrastructure may enable solving hard combinatorial problems.
Cloud providers are increasingly embracing network verification for managing complex datacenter network infrastructure. Microsoft's Azure cloud infrastructure integrates the SecGuru tool, which leverages the Z3 Satisfiability Modulo Theories (SMT) solver, for assuring that the network is configured to preserve desired intent over hundreds of thousands of network devices. We describe our experiences building and running SecGuru for network verification in Azure.
We then describe a distributed version of Z3 that scales with Azure's elastic cloud. It integrates recent advances in lookahead and distributed SAT solving for Z3's engines for SMT. A multi-threaded version of the Cube & Conquer solver is also available parallelizing SAT and SMT queries.
The contents of the talk is based on joint work with Marijn Heule, UT Austin; and Karthick Jayaraman, Rahul Kumar, Microsoft.