2026-06-19 –, C228 (capacity 24)
In this workshop, we demonstrate how engineers can write protocol specifications as code to systematically produce test scenarios for their systems. We focus on distributed systems that may fail in unexpected ways. We engage the audience in thinking about complex behaviors of distributed systems as runs of an executable specification, extending code with explicit non-determinism. This approach lets us distill complex system interactions while testing them against the actual deployment.
Our approach draws on years of experience building simulation tools and model checkers in both academia and industry. In the workshop, we:
- Write an executable specification and discuss modeling and abstraction patterns.
- Write executable tests (replacing whiteboard sequence diagrams).
- Generate tests via random and symbolic execution.
- Use the specification to drive adversarial tests of an implementation.
- Establish safety and liveness properties via model checking.
Igor Konnov is an independent security & formal methods researcher, practicing formal verification and fuzzing of distributed protocols. As a principal research scientist at Informal Systems and senior research scientist at Interchain Foundation, he has experience of integrating formal methods in the blockchain development process. Igor was the principal investigator in the projects Quint and Apalache. He worked as a researcher at Inria Nancy, TU Wien, and Lomonosov Moscow State University.
Thomas Pani works with software teams to build high-assurance systems. He applies advanced verification and falsification techniques (such as model-based testing, deterministic simulation, fuzzing, and model checking) to uncover subtle bugs in complex and distributed systems.
He holds a PhD in formal methods from TU Wien, has worked as a research engineer in both academia and industry, and is a core developer of the Apalache and Quint projects.