2023-09-10, 12:00–13:00 (Europe/Berlin), Tesla
Designing systems is difficult. Designing distributed systems is more difficult. Designing correct distributed systems becomes headache. In this talk, it will be shown how to approach towards more formal way of describing systems and what is motivation behind this approach. TLA+ and PlusCal will be shown as formal languages for formal system specification and how we can check our designs. During the talk, we will investigate some real world problems of real world systems and model-check them together!
Talk is about formal specification in TLA+ and PlusCal which are languages built with main goal to be precise and formally correct. These languages can be used to specify various kinds of systems, for us, software is clear example. They found applications mostly in distributed systems to ease process of designing distributed systems. Today, it is important to have precise and formal designs more than ever. For instance, discovering various security-related design issues becomes much easier.
My first project was financial analysis software. I also did software development in automotive industry and now my main focus is distributed systems. Currently working on distributed file server at Nutanix. We have to design and develop software which works on PB-scale data storage. When not building software, I am mentoring young computer science students in Petnica Science Center as head of computer science department. When I was young, I used to write articles for e-magazine about free software which was hosted by LUGoNS. Big lover of functional programming paradigm and math.