Thomas Pani
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.
Session
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.