Discover[i]: Component-based Parameterized Reasoning for Distributed Applications

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=GBqCKiborgY


Duration: 54:54
1,369 views
21

Distributed systems are hard to get right. There have been many notable efforts in formal reasoning for distributed systems: these efforts have focused on language design, automated or semi-automated verification, and, more recently, on automated synthesis for systems with a fixed number of processes. Our Discover[i] project seeks to automate aspects of programming distributed applications by developing new foundations, algorithms and tools for synthesis/verification of distributed applications built using (verified) components and parameterized by the number of processes.



In this talk, I will present an approach for parameterized synthesis of coordination for distributed systems that use consensus protocols, such as Paxos, as a building block to provide higher-level functionality. Our approach is based on (1) encapsulating the details of consensus into a simple atomic primitive, (2) a decidability result for parameterized verification of safety properties of systems with such consensus primitives, and (3) decision procedures for parameterized synthesis. We have used our tool to synthesize coordination for several examples of distributed applications, including a model of the Small Aircraft Tracking System.

See more at https://www.microsoft.com/en-us/research/video/discoveri-component-based-parameterized-reasoning-for-distributed-applications/



Other Videos By Microsoft Research


2019-10-14Reinforcement Learning From Small Data in Feature Space
2019-10-14Reward Machines: Structuring Reward Function Specifications and Reducing Sample Complexity...
2019-10-14Safe and Fair Reinforcement Learning
2019-10-14Scalable and Robust Multi-Agent Reinforcement Learning
2019-10-14Structure Visual Understanding and Interaction with Human and Environment
2019-10-14Improving Doctor-Patient Interaction with ML-Enabled Clinical Note Taking
2019-10-11HapSense: A Soft Haptic I/O Device with Uninterrupted Dual Functionalities...
2019-10-09Advanced polarized light microscopy for mapping molecular orientation
2019-10-09Data science and ML for human well-being with Jina Suh [Podcast]
2019-10-07Tea: A High-level Language and Runtime System for Automating Statistical Analysis [Python module]
2019-10-07Discover[i]: Component-based Parameterized Reasoning for Distributed Applications
2019-10-04Scheduling For Efficient Large-Scale Machine Learning Training
2019-10-03Distributed Entity Resolution for Computational Social Science
2019-10-03MMLSpark: empowering AI for Good with Mark Hamilton [Podcast]
2019-10-02Non-linear Invariants for Control-Command Systems
2019-10-02Vision-and-Dialog Navigation
2019-10-01The Future of Mathematics?
2019-09-30How Not to Prove Your Election Outcome
2019-09-30The Worst Form Including All Those Others: Canada’s Experiments with Online Voting
2019-09-30DIFF: A Relational Interface for Large-Scale Data Explanation
2019-09-30A Calculus for Brain Computation


Tags:
Distributed systems
Distributed Applications
Discover[i] project
Paxos
Small Aircraft Tracking System
algorithms
AI
machine learning
programming languages
microsoft research