Strange Loop Conference | "Formal Modeling and Analysis of Distributed Systems" by Ankush Desai (Strange Loop 2022) @StrangeLoopConf | Uploaded 1 year ago | Updated September 28 2023
Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about the myriad possible interleaving of messages and failures. Unsurprisingly, it is common to uncover bugs after deployment. Formal methods (FM) can play an important role in addressing this challenge. But the key requirement for “success” in is the ability to integrate FM in all the phases of development process from system design, implementation, to unit and integration testing, and even in production through runtime monitoring. In this talk, we will provide an overview of the P programming framework. P is a state machine-based programming language for modeling and specifying complex distributed systems. We will discuss how P is currently being used extensively inside Industry and Academia, addressing the challenges mentioned above. P is open-source.
Ankush Desai
Senior Applied Scientist, Amazon Web Services
@ankushpd
Ankush Desai is a Senior Applied Scientist in the Database Services (DBS) group at AWS. He is currently working on building formal tools and techniques that help developers reason about the correctness of complex distributed services across AWS (S3, DBS, EBS,). These techniques range from lightweight approaches like model checking, to systematic testing, to more rigorous deductive verification that provides mathematical proofs. . Before joining the DBS group, Ankush was part of the S3 team and worked on the Amazon S3's Strong Consistency project. Ankush graduated with a PhD in computer science from UC, Berkeley (2019). His PhD. research had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation. Before joining graduate school, Ankush spent 2+ years working at Microsoft Research, India working on formal verification of device drivers and distributed systems. Webpage: https://ankushdesai.github.io/
------ Sponsored by: ------
Stream is the # 1 Chat API for custom messaging apps. Activate your free 30-day trial to explore Stream Chat. https://gstrm.io/tsl
Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about the myriad possible interleaving of messages and failures. Unsurprisingly, it is common to uncover bugs after deployment. Formal methods (FM) can play an important role in addressing this challenge. But the key requirement for “success” in is the ability to integrate FM in all the phases of development process from system design, implementation, to unit and integration testing, and even in production through runtime monitoring. In this talk, we will provide an overview of the P programming framework. P is a state machine-based programming language for modeling and specifying complex distributed systems. We will discuss how P is currently being used extensively inside Industry and Academia, addressing the challenges mentioned above. P is open-source.
Ankush Desai
Senior Applied Scientist, Amazon Web Services
@ankushpd
Ankush Desai is a Senior Applied Scientist in the Database Services (DBS) group at AWS. He is currently working on building formal tools and techniques that help developers reason about the correctness of complex distributed services across AWS (S3, DBS, EBS,). These techniques range from lightweight approaches like model checking, to systematic testing, to more rigorous deductive verification that provides mathematical proofs. . Before joining the DBS group, Ankush was part of the S3 team and worked on the Amazon S3's Strong Consistency project. Ankush graduated with a PhD in computer science from UC, Berkeley (2019). His PhD. research had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation. Before joining graduate school, Ankush spent 2+ years working at Microsoft Research, India working on formal verification of device drivers and distributed systems. Webpage: https://ankushdesai.github.io/
------ Sponsored by: ------
Stream is the # 1 Chat API for custom messaging apps. Activate your free 30-day trial to explore Stream Chat. https://gstrm.io/tsl
