Portrait of Nikolaj Bjørner

Nikolaj Bjørner

Senior Principal Researcher

About

My main line of work is around the state-of-the-art SMT constraint solver Z3.  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.

  • 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 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

  • 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

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.

    • 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

Organization

  • I have had the joy of serving as program chair for several conferences, including PSI 2019, FMCAD 2018, ICDCIT 2016, FM 2015, LPAR 2012, CADE 2011.
  • I have been a recurrent co-chair for the Logic and Programming track at SYNASC with Laura Kovacs.
  • The next (8’th) Dagstuhl seminar I am co-organizing is Rigorous Methods for Smart Contracts
  • With Marijn Heule and Tachio Terauchi we hope the world looks better in 2022 for The Art of SAT at Shonan

Service

Awards