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.
- Z3: An Efficient SMT Solver (opens in new tab). As of 2021 with more than 7000 citations.
- Model-Based theory Combination (opens in new tab) 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 (opens in new tab) represents Z3’s architecture for combining decision procedures.
- Path Feasibility Analysis for String-Manipulating Programs (opens in new tab) previewed a significant development in the SMT community around string and regular expression (opens in new tab) solvers.
- Z3 is available from PyPi (opens in new tab), from Nuget (opens in new tab) and GitHub (opens in new tab) and downloaded roughly 35K times a month.
Selected Tutorial Material
- Programming Z3 (opens in new tab)
- Tutorial slides at SETSS 2018 (opens in new tab)
- Tutorial slides on quantifier solving, Mysore 2017 (opens in new tab)
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.
- Supercharging Plant Configurations using Z3 (opens in new tab) accompanies my keynote at CPAIOR 2021 (opens in new tab). 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 (opens in new tab) tool.
- muZ – an optimizing SMT solver (opens in new tab)
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.
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.
- 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.
- SecGuru and RCDC performs over 5 Billion Z3 queries a day when checking hundreds of thousands of routers in Azure (opens in new tab)
- Networks as Programs with George Varghese: NoD (opens in new tab), Symmetries and Surgeries (opens in new tab), ddNF, a SIGCOMM tutorial (opens in new tab).
- Controllers as reactive systems with Mooly Sagiv: VeriCon (opens in new tab)
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.
- 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.
- With Manya Ghobadi, Ishai Menache, Michael Schapira and collaborators: TeaVar (opens in new tab)
- With Rachee Singh, Sharon Shoham and collaborators: Shoofly (opens in new tab)
- With Rachee Singh and Michael Schapira: Cloud Traffic Engineering Tutorial (opens in new tab)
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 (opens in new tab): Universal PDR, Shoofly
- Marijn Heule: Cube and Conquer
- Marco Canini: Neural Networks for Networks
- Arie Gurfinkel (opens in new tab): SPACER in Z3
- Andrei Voronkov (opens in new tab): Verification of String Manipulating Programs, Hilbert Bases
- Assaf Schuster: Detection of latent faults in datacenters, distributed monitoring
- Rachee Singh (opens in new tab): Shoofly (opens in new tab) and Cloud Traffic Engineering Tutorial (opens in new tab)
- Karthick Jayaraman: SecGuru, RCDC, Network Change Verification System (NCVS), Azure Network Manager
- George Varghese (opens in new tab) Network Optimized Datalog, Symmetries and Surgeries, ddNF
- Nina Narodytska (opens in new tab): MaxSAT, Correction Set Enumeration, Binary Neural Network Verification
- Andrey Rybalchenko: Constrained Horn Clauses, Network Verification, Virtual Plant Configuration Optimization
- Laura Kovacs (opens in new tab): Algebraic methods in synthesis and verification
- Mooly Sagiv (opens in new tab): 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 (opens in new tab)
- Miguel Terra-Neves
- Sixue Liu
- Anh-Phan Dung
- Krystof Hoder
- Garvit Juniwal
- Nuno P. Lopes (opens in new tab)
- Mingchen Zhao
- Guido de Caso (opens in new tab)
- Sergio Mera
- Jannick Moy (opens in new tab)
- Ruzica Piskac (opens in new tab)
- Utkarsh Upadhyay (opens in new tab)
- Joe Hendrix (opens in new tab)
- Zachary Anderson
- Neil Conway
- 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 (opens in new tab)
- With Marijn Heule and Tachio Terauchi we hope the world looks better in 2022 for The Art of SAT at Shonan (opens in new tab)
- The scientific advisory board of Max Plank Institute for Informatics 2021 – 2025 (opens in new tab).
- Associate editor of Journal of Automated Reasoning (opens in new tab).
- Z3 received the 2015 ACM SIGPLAN Software System award (opens in new tab)
- Our paper on ddNF: An Efficient Data Structure for Header Spaces (opens in new tab) received a best paper award at HVC 2016
- Most influential tool paper in in the first 20 years of TACAS, 2017
- The paper on Efficient E-Matching for SMT Solvers (opens in new tab) received the 2017 Skolem Award at CADE (opens in new tab)
- The 2018 ETAPS test of time award (opens in new tab)
- Leonardo de Moura and I received the Herbrand Award at CADE 2019 (opens in new tab), in recognition of numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs
- I am a co-recipient of the 2021 CAV Award (opens in new tab) in recognition of pioneering contributions to SMT
- 2021 ACM Fellow
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…
[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…
“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,…