Supercharging Plant Configurations using Z3

Speaker: external pageNikolaj Bjørnercall_made, Microsoft Research
Time: Thursday, July 28, 9:15 - 11:15
Place: CAB G 59
Talk title: Supercharging Plant Configurations using Z3

DownloadTalk Slides (PDF, 8.2 MB)vertical_align_bottom

Abstract: 
We describe our experiences using Z3 for synthesizing and optimizing next generation plant configurations for a car manufacturing company [external page1call_made]. Our approach leverages unique capabilities of Z3: a combination of specialized solvers for finite domain bit-vectors and uninterpreted functions, and a programmable extension that we call constraints as code. To optimize plant configurations using Z3, we identify useful formalisms from Satisfiability Modulo Theories solvers and integrate solving capabilities for the resulting non-trivial optimization problems.

Bio: 
Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver external pageZ3call_made. 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 Nikolaj created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. He was named as 2021 ACM Fellow.