Portrait de Nikolaj Bjørner

Nikolaj Bjørner

Partner Researcher

À propos

My main line of work is around the state-of-the-art SMT constraint solver Z3 (opens in new tab).  Z3 was developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. The work around Z3 has received several awards. Karthick Jayaraman and I created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure and George Varghese introduced me to many insights around network verification and algorithmics. Until 2006, I was in the Core File Systems group where I designed and implemented the core of DFS-R which is included as part of Windows Server 2003 R2, Sharing Folders and Meetings Space.  I also designed some of the chunking utilities used in the remote differential compression protocol RDC. I was named as 2021 ACM Fellow.

Projects and Research

My main line of work spans development of symbolic solving techniques, networking and distributed file systems. Many of the symbolic techniques I develop are integral to Z3 and used in for software engineering applications, particularly managing cloud networks and broadly software and configurations.

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

    Highlights

    Selected Tutorial Material

    Other tutorial material is accessible from the repository and wiki pages on GitHub (opens in new tab).

  • 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

  • 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

  • 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 (opens in new tab) and instigated the use of model-based techniques for quantifier instantiation, MBQI (opens in new tab), 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 (opens in new tab), 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 (opens in new tab) 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 (opens in new tab) using Z3 for checking verification conditions of controllers. Network Verification is nowadays an integral topic in networking conferences with several systems using Z3.

    Highlights

  • 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 (opens in new tab) is a protocol deployed in 2006 for compressing network traffic. We have analyzed the algorithms used for Content dependent chunking (opens in new tab). 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 (opens in new tab)

  • 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

Some Current Activities

  • Smart Contracts have presented a match made in Blockchain heaven for verification techniques. Z3 is used in several systems that perform analysis of Smart Contracts. The bit-widths used in Ethereum byte code go well beyond the boundaries where SMT solving for bit-vectors have so far scaled. With Jakob Rath, TU Wien, we are developing more scalable algorithms for bit-vector arithmetic solving.
  • A new core for Z3. A long term development activity initiated in September 2020 is a new theory combination core for Z3. It is to replace and modernize the main core in Z3 that has been in use since 2010. With new cores come new capabilities: an integration of MBQI and quantifier elimination, in-processing for SMT, lazy bit-blasting, and many other goodies. Thorough testing is aided thanks to an active community that has developed powerful fuzzers for SMT solvers.

Collaborators and Interns

I have the fortune and luxury to be influenced by many stellar visitors, collaborators and interns.

Organization

Service

Awards

Contenu en vedette

Hyperscale cloud reliability and the art of organic collaboration

Hyperscale cloud reliability and the art of organic collaboration

What does it take to build one of the most reliable hyperscale clouds on the planet? It clearly requires astronomical investments and a vast organization that operates at global scale in near seamless coordination. Yet the breakthroughs that fuel this…

The inner magic behind the Z3 theorem prover

The inner magic behind the Z3 theorem prover

[caption id="attachment_614619" align="alignnone" width="1024"] Microsoft researchers Nikolaj Bjørner (left) and Leonardo de Moura (center) received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving. They’re pictured with Professor Jürgen Giesl…

SPACER and Z3: Accessible, reliable model checking as theorem proving

SPACER and Z3: Accessible, reliable model checking as theorem proving

“How can one check a routine in the sense of making sure that it is right?” asked Alan Turing in 1949, foreshadowing the science of program proving decades before it became a formally accepted field of computer science. Program proving,…