Weeks of Debugging Can Save You Hours of TLA+

This hands-on talk introduces TLA+ for specifying and verifying discrete systems, including concurrent and distributed algorithms. Participants use it to investigate a subtle concurrency failure through state machines, temporal logic, and computer-assisted verification.