diff --git a/content/lsd-seminar/2024fa.md b/content/lsd-seminar/2024fa.md index 08354dd..afd82ad 100644 --- a/content/lsd-seminar/2024fa.md +++ b/content/lsd-seminar/2024fa.md @@ -25,7 +25,7 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl | [Oct 25](#oct-25) | Haofan Zheng | Decentagram: Highly-Available Decentralized Publish/Subscribe Systems | | [Nov 1](#nov-1) | Justin Lubin | Programming By Navigation | | [Nov 8](#nov-8) | Bhakti Shah | Proof Visualization for Graphical Structures | -| [Nov 15](#nov-15) | Federico Mora | _TBD_ | +| [Nov 15](#nov-15) | Federico Mora | Automated Reasoning About Distributed Systems | | [Nov 22](#nov-22) | Haining Tong | _TBD_ | | [Dec 6](#dec-6) | Yanan Guo | _TBD_ | @@ -109,11 +109,13 @@ More broadly, I’ll talk about our deep, ongoing collaboration with experimenta **Speaker:** Federico Mora -**Title:** _TBD_ +**Title:** Automated Reasoning About Distributed Systems -**Abstract:** _TBD_ +**Abstract:** Designing and implementing distributed systems is still an enormous task for software engineers. Much of this challenge stems from the fact that bugs can arise from complex combinations of machine failures and message interleavings that are difficult for humans to reason about manually. As distributed systems become increasingly critical infrastructure, engineers will need more and more computational support to correctly build and deploy them. -**Bio:** _TBD_ +In this talk, I will present three automated reasoning techniques that can help software engineers build and deploy correct distributed systems. First, a domain-specific verification engine for message-passing distributed systems. Second, a decision procedure for a relevant fragment of logic. Third, a new approach for semi-automatically modelling distributed systems in a formal language. + +**Bio:** Federico Mora is a PhD candidate at the University of California, Berkeley, where he is advised by Sanjit A. Seshia. Federico’s research focuses on designing and implementing languages for automated reasoning. His studies have been supported by a Qualcomm Innovation Fellowship and three internships at Amazon Web Services, where he has applied many of the ideas described in his thesis. ## Nov 22