Nikolaj Bjørner

The Z3 solver was developed since 2006 and is today widely used across academia and industry in a wide range of applications.

Highlights

• Z3: An Efficient SMT Solver. As of 2021 with more than 7000 citations.
• Model-Based theory Combination is our first technical paper on Z3 and introduces a central theme in the design of theory solvers: they alternate model construction with refutation using dualities that are also fundamental to CDCL SAT solving, Linear Programming, and MIP.
• Generalized Efficient Array Decision Procedures represents Z3’s architecture for combining decision procedures.
• Path Feasibility Analysis for String-Manipulating Programs previewed a significant development in the SMT community around string and regular expression solvers.
• Z3 is available from PyPi, from Nuget and GitHub and downloaded roughly 35K times a month.

Selected Tutorial Material

• Programming Z3
• Tutorial slides at SETSS 2018
• Tutorial slides on quantifier solving, Mysore 2017

Other tutorial material is accessible from the repository and wiki pages on GitHub.

When SAT is not enough, Optimization Modulo Theories allows to ask SMT queries and simultaneously optimize for objectives. Z3 integrates algorithms for optimizing linear constraints over reals and integers and weighted MaxSAT. Optimization Modulo Theories shines when the applications benefit from theories supported in Z3. In contrast to contemporary operations research tools, Z3 allows modeling with uninterpreted functions that offer sometimes dramatic savings over indicator variables. Other supported theories, such as algebraic datatypes by Zvonimir Pavlinovic, have been of of use as well.

Highlights

• Supercharging Plant Configurations using Z3 accompanies my keynote at CPAIOR 2021. It describes experiences with an Azure customer from the automotive space and algorithmic secret sauce.
• Z3 integrates special algorithms for consequence finding. The algorithms integrate with efficient CDCL search and they are used in the Microsoft Dynamics Configurator tool.
• muZ – an optimizing SMT solver

Symbolic model checking of safety properties can be represented as a constraint solving problem of quantified Horn clauses. Andrey Rybalchenko further recognized that most proof rules for used for deductive verification can be reformulated as Constrained Horn Clause solving. In 2012, Krystof Hoder and I developed a solver for Horn Clauses over linear arithmetic constraints by reformulating Aaron Bradley’s IC3 modulo theories and for non-linear Horn Clauses. Non-linear Horn Clauses are useful for modeling procedure calls: each uninterpreted predicate in a body corresponds to summarizing a recursive procedure call. The implementation became a default Horn Clause solver in Z3 along with a solver, Duality, by Ken McMillan. The solvers are now replaced by the SPACER solver by Arie Gurfinkel. SPACER extends the original PDR solver with crucial innovations on unfolding non-linear Horn clauses.

Highlights

• Generalized Property Directed Reachability
• Horn Clause solvers for Program Verification
• SPACER and Arie Gurfinkel

SMT problems from verification often involve quantified formulas. Unlike saturation-based theorem provers, instantiation based techniques are so far dominant in the context of theory reasoning. We have developed several different algorithms for respective classes of formulas.

Highlights

• With Leonardo de Moura I developed incremental term indexing for efficient E-matching and instigated the use of model-based techniques for quantifier instantiation, MBQI, developed in substance by Leonardo de Moura and collaborators. These two techniques are the foundation for quantified solving in Z3 integrating theory reasoning.
• Mikolas Janota’s algorithms for QBF formed the foundation for quantifier satisfiability solving modulo theories, QSAT, in Z3.
• Constrained Horn Clauses are naturally also quantified. When their symbolic solutions and background axiomatizations require quantifiers, as is the case for theories of heap properties, the related Universal PDR algorithm can be used to automatically synthesize universal invariants. It was developed in collaboration with Mooly Sagiv, Shachar Itzhaky, Aditya Thakur, Tom Reps, Alexander Karbyshev, and Sharon Shoham.

My journey in Network Verification started when Karthick Jayaraman attended a talk by Vijay Ganesh whom I was hosting for a short visit. Karthick was introduced and came by to discuss his task on ensuring reliability of network access policies in Azure datacenters. It was still early days for Azure. We quickly realized the power of declarative modeling using Z3 for network ACLs and deployed a checker for ACLs named SecGuru widely in Azure. Network Verification gained steam when George Varghese arrived to Microsoft Research and instigated the perspective of networks as programs and algorithmic techniques for reachability properties. We developed Network Optimized Datalog with Nuno Lopes, which an initial seed for Sean McLaughlin and Byron Cook at AWS in their work on Tiros. Gordon Plotkin introduced us symmetry/bi-simulation techniques, well-known for programming language semantics, but now applied to networks. Mooly Sagiv spearheaded VeriCon using Z3 for checking verification conditions of controllers. Network Verification is nowadays an integral topic in networking conferences with several systems using Z3.

Highlights

• SecGuru and RCDC performs over 5 Billion Z3 queries a day when checking hundreds of thousands of routers in Azure
• Networks as Programs with George Varghese: NoD, Symmetries and Surgeries, ddNF, a SIGCOMM tutorial.
• Controllers as reactive systems with Mooly Sagiv: VeriCon

I devoted the years 2000 – 2006 to the development and deployment of distributed file systems. The period culminated with the release of the DFSR replication component which was integral in the Windows Server release in late 2005.

Highlights

• DFSR – The Distributed File System Replication systems was deployed in Windows server editions from 2006, for about a decade onwards. It performs multi-master file replication on Windows server instances. It was also used in the Windows Messenger 8 for P2P file sharing by an estimated 40M users.
• RDC is a protocol deployed in 2006 for compressing network traffic. We have analyzed the algorithms used for Content dependent chunking. Nadim Abdo and I later developed a specialized chunking algorithm tuned for buffers used by RDP (Remote Desktop Protocol used to access Windows desktops remotely)
• To test and validate our protocols and implementation we applied methods from model checking and built a distributed simulation environment

Network traffic engineering has emerged as an exciting area for cloud based WANs. Cloud based WANs maintain capabilities for making global measurements, predictions, prioritize and schedule traffic. Microsoft’s SWAN solves flow constraints for network demands to optimize traffic flows. I have had a privilege to contribute with a few tweaks in SWAN’s solver and develop a solver that was used to plan a doubling of SWAN’s network. I am currently working with Rachee Singh on algorithms for solving provisioning constraints.

Higlights

• With Manya Ghobadi, Ishai Menache, Michael Schapira and collaborators: TeaVar
• With Rachee Singh, Sharon Shoham and collaborators: Shoofly
• With Rachee Singh and Michael Schapira: Cloud Traffic Engineering Tutorial

• Sharon Shoham: Universal PDR, Shoofly
• Marijn Heule: Cube and Conquer
• Marco Canini: Neural Networks for Networks
• Arie Gurfinkel: SPACER in Z3
• Andrei Voronkov: Verification of String Manipulating Programs, Hilbert Bases
• Assaf Schuster: Detection of latent faults in datacenters, distributed monitoring

• Rachee Singh: Shoofly and Cloud Traffic Engineering Tutorial
• Karthick Jayaraman: SecGuru, RCDC, Network Change Verification System (NCVS), Azure Network Manager
• George Varghese Network Optimized Datalog, Symmetries and Surgeries, ddNF
• Nina Narodytska: MaxSAT, Correction Set Enumeration, Binary Neural Network Verification
• Andrey Rybalchenko: Constrained Horn Clauses, Network Verification, Virtual Plant Configuration Optimization
• Laura Kovacs: Algebraic methods in synthesis and verification
• Mooly Sagiv: Network Controller verification, Universal PDR, Verification of Smart Contracts
• Nuno P. Lopes: Network Optimized Datalog and Alive. Nuno was once an intern.
• Daniel Selsam: Neural Networks to speed up SAT solving.
• Leonardo de Moura: Z3
• Christoph Wintersteiger: Z3
• Lev Nachmanson: Z3
• Margus Veanes: Regular Expressions, Transducers, Z3

• Max Levatich
• Daniel Selsam
• Miguel Terra-Neves
• Sixue Liu
• Anh-Phan Dung
• Krystof Hoder
• Garvit Juniwal
• Nuno P. Lopes
• Mingchen Zhao
• Guido de Caso
• Sergio Mera
• Jannick Moy
• Ruzica Piskac
• Utkarsh Upadhyay
• Joe Hendrix
• Zachary Anderson
• Neil Conway