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.
- 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
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.
- 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.
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 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.
- 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.
- 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.
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.
- 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
- 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
- The scientific advisory board of Max Plank Institute for Informatics 2021 – 2025.
- Associate editor of Journal of Automated Reasoning.
- Z3 received the 2015 ACM SIGPLAN Software System award
- Our paper on ddNF: An Efficient Data Structure for Header Spaces 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 received the 2017 Skolem Award at CADE
- The 2018 ETAPS test of time award
- Leonardo de Moura and I received the Herbrand Award at CADE 2019, 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 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,…