Software Modeling with TLA+ Workshop

Hillel Wayne

<p>Most software ﬂaws come from one of two places. When the code doesn’t match our expectations, it could be that the code is wrong. Most software correctness techniques - types, tests, etc - are used to check the code. But it could instead be that the code is correct and our expectations are wrong: there’s a fundamental error in our model of the system. These bugs are the most difficult to find and the most expensive to fix. Our standard techniques cannot handle them.</p><p>The answer to this is software modeling. By writing out the design in a software modeling tool, we can directly test the design for bugs <em>without having to write any code first.</em> Modeling software leads to simpler, safer systems built more quickly and cheaply. </p><p>One such modeling tool is TLA+. TLA+ is designed to model concurrent and distributed systems, and has been successfully to find bugs in everything from <a href="https://www.cslab.pepperdine.edu/warford/math221/How-Amazon-Web-Services-Uses-Formal-Methods.pdf" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">cloud services</a> and <a href="https://www.youtube.com/watch?v=oMSmkRGzQ64" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">message queues</a> to video games and <a href="https://dl.acm.org/doi/10.5555/1779934.1779955" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">embedded operating systems</a>.</p><p>In this class you will learn the basics of TLA+ from one of the foremost experts on teaching formal methods.  After the class, you will get an opportunity for private feedback on a TLA+ spec you write.</p><h2>Structure</h2><p>Class will be one day by Zoom. Students will learn the conceptual core of TLA+, why and how it works, and then use it to write simple specifications. While the class is not comprehensive, it will give students the strongest foundation possible to learn auxiliary topics. Supplementary material, including references, cheat sheets, and extra credit, will be provided.</p><h2>Audience</h2><p>Attendees should have some experience programming and some experience testing. While TLA+ is extremely powerful, it is best used by experienced programmers. Some knowledge of formal logic is helpful but not necessary, and will be covered in the class itself.</p><p>It is best if students have prior experience with VSCode. </p><h2>About the Instructor</h2><p><a href="https://www.hillelwayne.com" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">Hillel Wayne</a> is a formal methods educator and consultant. He is the author of <a href="https://learntla.com/" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">Learn TLA+</a>, <a href="https://www.amazon.com/Practical-TLA-Planning-Driven-Development/dp/1484238281" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">Practical TLA+</a>, and <a href="https://alloy.readthedocs.io/en/latest/" target="_blank" data-msys-clicktrack="0" rel="nofollow noopener noreferrer">alloydocs</a>. His past clients include Facebook, Cigna, Crowdstrike, and NASA.</p>

Our {communityGuidelinesLink} describe the sort of content we prohibit on Eventbrite. If you suspect an event may be in violation, you can report it to us so we can investigate.

To report other categories of prohibited or illegal content, submit {link}

Software Modeling with TLA+ Workshop

More events from Hillel Wayne

Discover more events from Hillel Wayne, from Science & Tech to other experiences you might love.

Still looking for the right event?

Explore all online events to browse and filter by date, category, and more.

Software Modeling with TLA+ Workshop

More events from Hillel Wayne

Discover more events from Hillel Wayne, from Science & Tech to other experiences you might love.

You might also like...

Browse more events with different dates, prices, and formats to find your next great experience.

Still looking for the right event?

Explore all online events to browse and filter by date, category, and more.