COMPUTER SCIENCE RESEARCH WEEK 2019

Formal Methods and Tools for Distributed Systems

Speaker
Dr Thomas Ball, Principal Researcher, Microsoft Research
Contact Person
Dr Reza SHOKRI, Associate Professor, School of Computing
reza@comp.nus.edu.sg

09 Jan 2019 Wednesday, 10:00 AM to 11:30 AM

SR1, COM1-02-06

This is a distinguished talk as part of the NUS Computer Science Research Week 2019 (http://researchweek.comp.nus.edu.sg).

Abstract:

Microsoft is a leader in the development and deployment of tools for distributed systems based on formal methods, the mathematical/logical specification, design and verification of systems. In this talk, I'll give an overview of some of the key methods and tools that are in regular use in Microsoft's Azure Cloud Computing Platform, which range from mathematical specification of high-level design (TLA+), programming and systematic testing of protocols (P# and Ivy), and the automated checking of network and firewall configurations (SecGuru). Many of these tools address difficult verification problems by reduction to logic and the application of automated theorem proving (Z3). TLA+, P#, Ivy, and Z3 are all open source technologies made available to the wider community (https://github.com/tlaplus, https://github.com/p-org/, https://github.com/Microsoft/ivy, https://github.com/Z3Prover, https://github.com/Z3Prover/FirewallChecker).

The talk starts with a tutorial on the preliminaries and the theoretical foundations of this topic.


Biodata:

Thomas (Tom) Ball is a principal researcher and manager at Microsoft Research. In 1999, He initiated the influential SLAM software model-checking project with Sriram Rajamani, which led to the creation of the Static Driver Verifier tool for finding defects in Windows device drivers. Tom is a 2011 ACM Fellow for 'contributions to software analysis and defect detection'. As a manager, he has nurtured research areas such as automated theorem proving, program testing/verification and empirical software engineering. His current focus is the Microsoft Makecode platform for programming with physical computers.