USI - Email

Archive / INF Seminars / INF_2023_03_20_Nikolaj_Bjorner

USI - Email

	Overview of formal method tools from Microsoft Research

Host: Prof. Natasha Sharygina

Monday

20.03

USI Campus Est, room D1.14, Sector D

10:30 - 11:30


	Nikolaj Bjorner Microsoft Research, Redmond, USA

Abstract: The lecture provides an overview of several formal methods tools from Microsoft Research and their uses in products. Many of the tools are based on solving symbolic logic formulas using the SMT solver Z3. With the perspective of applications in program verification, virtual plant configurations, and network verification we outline some main algorithmic ingredients in z3.

Biography: Nikolaj Bjorner is a partner researcher at Microsoft Research. Nikolaj’s 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 Nikolaj created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. In 2021 Nikolaj Bjorner was named an ACM Fellow.