Formal Methods and Tools for Distributed Systems
COM1 Level 2
SR1, COM1-02-06
closeThis 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.