Invited talk at VSTTE 2024

It was my pleasure to participate in VSTTE24 and give an invited talk there, mainly about Apalache. Since I had a break in academic conferences, I was pleasantly surprised by practical focus of this academic conference. Since the conference was held entirely offline, there are no recordings. However, you can read my blogpost, which I started to write right on the train from Prague to Vienna.

If you wonder what the talk was about, here is the abstract:

TLA⁺ continues to be the preferred specification language for fault-tolerant distributed algorithms, especially, for distributed consensus. Although consensus algorithms have relatively concise specifications, analyzing their behavior is notoriously difficult due to the inherent control and data non-determinism arising from their distributed nature and potential Byzantine faults. In this talk, I will showcase the spectrum of guarantees that can be obtained in reasonable time using the Apalache model checker. I will also discuss the usability aspects of both TLA⁺ and Apalache for system engineers.