Igor Konnov
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.
Independent security and formal methods researcher
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.