Building a Foundation for Verification of Distributed Systems in Iris

Jonas Kastberg Hinrichsen

Formal Verification is quite an undertaking, even for simple systems, with specifications and approaches quickly growing beyond the scope of which one can maintain a proper overview. This is doubly true for more complicated systems, like those utilizing concurrency and distributed communication; as such it is imperative to employ intuitive methods to alleviate possible overhead.

In recent years, much work has been done on establishing common ground for verification. One particularly interesting approach is that of the logical framework Iris, which include many high-level features, such as higher-order predicates as well as a foundation for concurrency.

As for communication properties, the state-of-the-art solution, which is continuously being expanded, is the Session Type protocol typing system, that guarantees notions such as deadlock freedom through well-typedness.

The talk will thus consist of an overview of the intended goals of the research, namely combining Session Types with Iris, while focusing on the underlying theory and how I plan to put them together.

---

Previous: Léon Gondelman | Semi-Automated Reasoning About Non-Determinism in C Expressions
Next: TBA | TBA