Events
29
September
2022
29.
09.
2022
06
October
2022
06.
10.
2022
07
October
2022
07.
10.
2022
13
October
2022
13.
10.
2022
20
October
2022
20.
10.
2022
27
October
2022
27.
10.
2022

Supercharging Plant Configurations using Z3

Staff - Faculty of Informatics

Date: 29 April 2022 / 10:30 - 11:30

USI Lugano Campus EST, room D0.02, Sector D // Online on MS Teams

Click here to join

Speaker: Nikolaj Bjorner, Microsoft Research Redmond

Abstract: 
We describe our experiences using Z3 for synthesizing and optimizing next generation plant configurations for a car manufacturing company1. 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.

Biography:
Nikolaj Bjorner is a senior researcher in the Research in Software Engineering group at Microsoft Research, Redmond. His main line of work is around the state-of-the-art SMT constraint solver Z3 with Leonardo de Moura. Z3 is used for program verification and test case generation.

Host: Prof. Natasha Sharygina