Abstract:

Configurations form a basis for deploying infrastructure and custom instances in today’s hyperscale cloud environments. Similar to conventional program analysis, configurations can be subjected to logical specifications and checked for correctness claims. In contrast to program analysis, the analysis relies on information from, and provides feedback on the health of, live systems.

This talk takes as starting point some of the experiences with using the SMT solver Z3 for checking declarative configurations in the Azure cloud. It then describes solving techniques applied for checking configurations, and SMT formulas in general. A theme characterizing these solving techniques is how they combine search for a model with deducing logical consequences. The talk provides exemplars of how search and consequence finding is integrated in Z3.

Biography:

Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS, and the ETAPS test of time award. Leonardo and Nikolaj 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. A prolific application is around Network Verification as deployed in the SecGuru tool in Microsoft Azure. In previous work in the Windows File Systems group, he developed the Distributed File System Replication, DFS-R, protocol. He studied at DTU, DIKU; and for his Master’s and PhD at Stanford.

Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS, and the ETAPS test of time award. Leonardo and Nikolaj 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. A prolific application is around Network Verification as deployed in the SecGuru tool in Microsoft Azure. In previous work in the Windows File Systems group, he developed the Distributed File System Replication, DFS-R, protocol. He studied at DTU, DIKU; and for his Master’s and PhD at Stanford.