Microsoft Research, USA
Abstract
The talk presents several research projects and tools from Microsoft Research and their impact on programming secure and reliable systems.As a common basis they take a formal methods angle where systems are viewed as mathematical objects and consider computation through lenses of calculi and measurements. We then describe how these research threads interleave with major developments from academic research and phase shifts in industry.With Microsoft rapidly pivoting on deploying and delivering AI products the talk connects foundations with current projects, including development of provably secure systems,
securing smart contracts, network verification, efficient and correct compilation for ML systems, and programming systems and runtimes for interacting with AI.
Short Bio
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. He was named as 2021 ACM Fellow. He is presently a partner research manager at Microsoft Research, Redmond.